aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Natural/Binary
Commit message (Expand)AuthorAge
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Updating headers.Gravatar herbelin2012-08-08
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Modularization of BinNat + fixes of stdlibGravatar letouzey2011-05-05
* An automatic substitution of scope at functor applicationGravatar letouzey2011-02-11
* Annotations at functor applications:Gravatar letouzey2011-02-11
* Numbers: simplier spec for testbitGravatar letouzey2011-01-20
* Numbers: some improvements in proofsGravatar letouzey2011-01-03
* Numbers and bitwise functions.Gravatar letouzey2010-12-06
* Integer division: quot and rem (trunc convention) in addition to div and modGravatar letouzey2010-11-10
* Numbers: axiomatization, properties and implementations of gcdGravatar letouzey2010-11-05
* NZSqrt : since spec is complete, no need for morphism axiom sqrt_wdGravatar letouzey2010-11-02
* NZLog : since spec is complete, no need for morphism axiom log2_wdGravatar letouzey2010-11-02
* Numbers : log2. Abstraction, properties and implementations.Gravatar letouzey2010-11-02
* Numbers: specs about sqrt and pow of neg numbers, even in NZGravatar letouzey2010-11-02
* Add sqrt in NumbersGravatar letouzey2010-10-19
* Numbers : also axiomatize constants 1 and 2.Gravatar letouzey2010-10-14
* Numbers: new functions pow, even, odd + many reorganisationsGravatar letouzey2010-10-14
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Made option "Automatic Introduction" active by default before too manyGravatar herbelin2010-06-08
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Euclidean division for NArithGravatar letouzey2010-02-10
* NBinary improved, contains more, subsumes NOrderedTypeGravatar letouzey2010-02-09
* Avoid some more re-declarations of Equivalence instancesGravatar letouzey2010-01-14
* Support "Local Obligation Tactic" (now the default in sections).Gravatar msozeau2010-01-11
* Simplification of Numbers, mainly thanks to IncludeGravatar letouzey2009-11-10
* Numbers: finish files NStrongRec and NDefOpsGravatar letouzey2009-11-06
* Numbers: more (syntactic) changes toward new style of type classesGravatar letouzey2009-11-06
* Numbers: start using Classes stuff, Equivalence, Proper, Instance, etcGravatar letouzey2009-11-03
* Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'Gravatar letouzey2009-10-08
* In abstract parts of theories/Numbers, plus/times becomes add/mul, Gravatar letouzey2008-06-03
* In abstract parts of theories/Numbers, plus/times becomes add/mul, Gravatar letouzey2008-06-02
* switch theories/Numbers from Set to Type (both the abstract and the bignum pa...Gravatar letouzey2008-05-22
* Coq headers + $ in theories/Numbers filesGravatar letouzey2008-05-15
* Definition of N moves back to BinNat (partial backtrack of commits 10298-10300)Gravatar letouzey2008-04-16
* Update on Numbers; renamed ZOrder.v to ZLt to remove clash with ZArith/Zorder...Gravatar emakarov2007-11-14
* Replaced BinNat with a new version that is based on theories/Numbers/Natural/...Gravatar emakarov2007-11-07
* An update of theories/NumbersGravatar emakarov2007-11-03
* Added Numbers/Natural/Abstract/NIso.v that proves that any two models of natu...Gravatar emakarov2007-10-23
* Added the compilation of theories/Numbers to Makefile.common. The following t...Gravatar emakarov2007-10-01
* An update on theories/Numbers.Gravatar emakarov2007-09-25
* Update on theories/Numbers. Natural numbers are mostly complete,Gravatar emakarov2007-09-21
* Update before joining all signatures into one.Gravatar emakarov2007-09-13
* An update on axiomatic number classes.Gravatar emakarov2007-08-13
* An update on axiomatization of number classes.Gravatar emakarov2007-07-13
* Update of theories/Numbers directory.Gravatar emakarov2007-07-06
* Added the directory theories/Numbers where axiomatizations and implementation...Gravatar emakarov2007-06-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 11:23:53 +0000