aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Integer/Binary
Commit message (Expand)AuthorAge
* Updating headers.Gravatar herbelin2012-08-08
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Modularization of BinInt, related fixes in the 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
* ZArith: for uniformity, Zdiv2 becomes Zquot2 while Zdiv2' becomes Zdiv2Gravatar letouzey2010-12-09
* Numbers and bitwise functions.Gravatar letouzey2010-12-06
* Division: avoid imposing rem as an infix keyword in Z_scope and bigZ_scope.Gravatar letouzey2010-11-16
* 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
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* ZBinary (impl of Numbers via Z) reworked, comes earlier, subsumes ZOrderedTypeGravatar 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
* Numbers: axiomatization + generic properties of abs and sgn.Gravatar letouzey2010-01-08
* RelationPairs: stop loading it in all Numbers, stop maximal args with fst/sndGravatar letouzey2009-12-18
* Simplification of Numbers, mainly thanks to IncludeGravatar letouzey2009-11-10
* 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
* 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
* - Changement du code de Zplus pour accomoder ring qui sinon prend uneGravatar herbelin2008-05-11
* 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
* Added Numbers/Natural/Abstract/NIso.v that proves that any two models of natu...Gravatar emakarov2007-10-23
* Added transitivity and irreflexivity of <, as well as < -elimination for bina...Gravatar emakarov2007-10-16
* The following now compiles: abstract integers with plus, minus and times, bin...Gravatar emakarov2007-10-02
* Added the compilation of theories/Numbers to Makefile.common. The following t...Gravatar emakarov2007-10-01
* Update on theories/Numbers. Natural numbers are mostly complete,Gravatar emakarov2007-09-21