src/HOL/Integ/IntDef.thy
2006-01-23 haftmann 2006-01-23 removed problematic keyword 'atom'
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-18 haftmann 2006-01-18 substantial improvement in serialization handling
2006-01-17 haftmann 2006-01-17 substantial improvements in code generator
2005-12-29 haftmann 2005-12-29 adaptions to changes in code generator
2005-12-02 haftmann 2005-12-02 adjusted to improved code generator interface
2005-11-22 haftmann 2005-11-22 added codegenerator
2005-11-08 haftmann 2005-11-08 (fix for accidental commit)
2005-11-08 haftmann 2005-11-08 (codegen)
2005-09-27 berghofe 2005-09-27 Inserted clause for nat in number_of_codegen again ("code unfold" turned out to be too inefficient).
2005-09-21 berghofe 2005-09-21 Simplified code generator for numerals.
2005-09-17 wenzelm 2005-09-17 added quickcheck_params (from Main.thy);
2005-08-16 paulson 2005-08-16 more simprules now have names
2005-07-12 berghofe 2005-07-12 Auxiliary functions to be used in generated code are now defined using "attach".
2005-07-07 nipkow 2005-07-07 linear arithmetic now takes "&" in assumptions apart.
2005-07-01 berghofe 2005-07-01 Moved code generator setup from NatBin to IntDef.
2005-06-16 paulson 2005-06-16 a few new integer lemmas
2005-05-04 nipkow 2005-05-04 Fixing a problem with lin.arith.
2005-03-02 paulson 2005-03-02 new lemmas int_diff_cases
2005-03-01 nipkow 2005-03-01 integrated Jeremy's FiniteLib
2005-02-21 nipkow 2005-02-21 removed superfluous setsum_constant
2005-02-21 nipkow 2005-02-21 comprehensive cleanup, replacing sumr by setsum
2005-02-01 paulson 2005-02-01 the new subst tactic, by Lucas Dixon
2004-12-15 paulson 2004-12-15 removal of archaic Abs/Rep proofs
2004-12-14 paulson 2004-12-14 new and stronger lemmas and improved simplification for finite sets
2004-11-19 paulson 2004-11-19 moved and renamed Integ/Equiv.thy
2004-10-19 paulson 2004-10-19 converted some induct_tac to induct
2004-09-01 paulson 2004-09-01 new "respects" syntax for quotienting
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-07-15 paulson 2004-07-15 redefining sumr to be a translation to setsum
2004-07-01 paulson 2004-07-01 new treatment of binary numerals
2004-06-24 paulson 2004-06-24 replaced monomorphic abs definitions by abs_if
2004-05-12 nipkow 2004-05-12 fixed latex problems
2004-05-11 obua 2004-05-11 changes made due to new Ring_and_Field theory
2004-05-01 wenzelm 2004-05-01 tuned instance statements;
2004-04-23 paulson 2004-04-23 congruent2 now allows different equiv relations
2004-04-08 paulson 2004-04-08 tidied
2004-03-30 paulson 2004-03-30 tidied
2004-03-25 paulson 2004-03-25 new material from Avigad
2004-03-24 paulson 2004-03-24 streamlined treatment of quotients for the integers
2004-03-04 paulson 2004-03-04 new material from Avigad, and simplified treatment of division by 0
2004-03-01 paulson 2004-03-01 new Ring_and_Field hierarchy, eliminating redundant axioms
2004-02-19 ballarin 2004-02-19 Efficient, graph-based reasoner for linear and partial orders. + Setup as solver in the HOL simplifier.
2004-02-15 paulson 2004-02-15 Polymorphic treatment of binary arithmetic using axclasses
2004-02-10 paulson 2004-02-10 generic of_nat and of_int functions, and generalization of iszero and neg
2004-01-09 paulson 2004-01-09 Defining the type class "ringpower" and deleting superseded theorems for types nat, int, real, hypreal
2004-01-06 paulson 2004-01-06 Ring_and_Field now requires axiom add_left_imp_eq for semirings. This allows more theorems to be proved for semirings, but requires a redundant axiom to be proved for rings, etc.
2003-12-03 paulson 2003-12-03 Simplification of the development of Integers
2003-11-28 paulson 2003-11-28 conversion of some Real theories to Isar scripts
2003-11-18 paulson 2003-11-18 conversion of ML to Isar scripts
2002-08-08 wenzelm 2002-08-08 tuned;
2001-10-22 paulson 2001-10-22 Numerals now work for the integers: the binary numerals for 0 and 1 rewrite to their abstract counterparts, while other binary numerals work correctly.
2001-10-08 wenzelm 2001-10-08 sane numerals (stage 3): provide generic "1" on all number types;
2001-10-05 wenzelm 2001-10-05 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
2001-07-25 paulson 2001-07-25 partial restructuring to reduce dependence on Axiom of Choice
2001-01-09 nipkow 2001-01-09 *** empty log message ***
2001-01-05 nipkow 2001-01-05 ^^ -> ``` Univalent -> single_valued
2000-10-13 nipkow 2000-10-13 *** empty log message ***
2000-10-12 nipkow 2000-10-12 *** empty log message ***