src/HOL/Nat.thy
2006-11-22 haftmann 2006-11-22 cleanup
2006-11-18 haftmann 2006-11-18 power is now a class
2006-11-08 wenzelm 2006-11-08 removed obsolete nat_case_tr' (duplicates case_tr' in datatype_package.ML);
2006-11-08 wenzelm 2006-11-08 removed theory NatArith (now part of Nat);
2006-11-06 haftmann 2006-11-06 code generator module naming improved
2006-10-16 haftmann 2006-10-16 added explicit print translation for nat_case
2006-10-02 haftmann 2006-10-02 added code generator names for nat_rec and nat_case
2006-09-26 haftmann 2006-09-26 renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
2006-09-25 haftmann 2006-09-25 refinements in codegen serializer
2006-09-20 haftmann 2006-09-20 name shifts
2006-09-19 haftmann 2006-09-19 added operational equality
2006-08-14 haftmann 2006-08-14 simplified code generator setup
2006-08-08 haftmann 2006-08-08 cleanup code generation for Numerals
2006-06-14 haftmann 2006-06-14 slight adaption for code generator
2006-06-13 paulson 2006-06-13 new results
2006-05-05 wenzelm 2006-05-05 axiomatization;
2006-01-17 haftmann 2006-01-17 substantial improvements in code generator
2006-01-11 paulson 2006-01-11 tidied, and giving theorems names
2005-09-29 wenzelm 2005-09-29 more finalconsts;
2005-09-22 nipkow 2005-09-22 renamed rules to iprover
2005-07-13 paulson 2005-07-13 generlization of some "nat" theorems
2005-07-07 nipkow 2005-07-07 linear arithmetic now takes "&" in assumptions apart.
2005-07-01 berghofe 2005-07-01 Moved some code lemmas from Main to Nat.
2005-05-04 nipkow 2005-05-04 Fixing a problem with lin.arith.
2005-02-21 nipkow 2005-02-21 comprehensive cleanup, replacing sumr by setsum
2004-12-15 paulson 2004-12-15 removal of archaic Abs/Rep proofs
2004-11-29 paulson 2004-11-29 converted to Isar script, simplifying some results
2004-11-13 nipkow 2004-11-13 More lemmas
2004-10-19 paulson 2004-10-19 converted some induct_tac to induct
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
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-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-27 paulson 2003-12-27 re-organized numeric lemmas
2003-12-19 nipkow 2003-12-19 *** empty log message ***
2003-11-25 paulson 2003-11-25 More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas to Isar script.
2003-11-24 paulson 2003-11-24 conversion of integers to use Ring_and_Field; new lemmas for Ring_and_Field
2003-11-21 paulson 2003-11-21 HOL: installation of Ring_and_Field as the basis for Naturals and Reals
2003-09-26 paulson 2003-09-26 misc tidying
2003-09-22 berghofe 2003-09-22 Improved efficiency of code generated for + and -
2003-07-24 paulson 2003-07-24 declarations moved from PreList.thy
2002-09-30 nipkow 2002-09-30 modified induct method
2002-09-26 paulson 2002-09-26 Converted Fun to Isar style. Moved Pi, funcset, restrict from Fun.thy to Library/FuncSet.thy. Renamed constant "Fun.op o" to "Fun.comp"
2002-08-05 berghofe 2002-08-05 - Converted to new theory format - Moved NatDef stuff to theory Nat
2001-12-01 wenzelm 2001-12-01 renamed class "term" to "type" (actually "HOL.type");
2001-07-25 paulson 2001-07-25 partial restructuring to reduce dependence on Axiom of Choice
2001-05-22 berghofe 2001-05-22 Inductive definitions are now introduced earlier in the theory hierarchy.
2001-02-15 oheimb 2001-02-15 added nat as instance of new wellorder axclass
2000-11-10 wenzelm 2000-11-10 added axclass power (from HOL.thy);
2000-07-25 wenzelm 2000-07-25 rearranged setup of arithmetic procedures, avoiding global reference values;
1999-10-04 wenzelm 1999-10-04 removed DatatypePackage.setup;
1998-10-21 berghofe 1998-10-21 Changed syntax of rep_datatype.
1998-09-18 paulson 1998-09-18 updated comments
1998-07-24 berghofe 1998-07-24 Declaration of type 'nat' as a datatype (this allows usage of exhaust_tac and induct_tac on type 'nat'). Moved some proofs using natE from NatDef.ML to Nat.ML.
1998-02-20 nipkow 1998-02-20 Congruence rules use == in premises now. New class linord.
1998-02-09 nipkow 1998-02-09 Replaced ALLNEWSUBGOALS by THEN_ALL_NEW
1997-11-03 wenzelm 1997-11-03 nat datatype_info moved to Nat.thy;