src/HOL/Nat.thy
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;
1997-05-30 paulson 1997-05-30 Overloading of "^" requires new type class "power", with types "nat" and "set" in that class. The operator itself is declared in Nat.thy
1997-02-12 nipkow 1997-02-12 New class "order" and accompanying changes. In particular reflexivity of <= is now one rewrite rule.
1997-01-23 wenzelm 1997-01-23 removed \<mu> syntax;
1996-12-13 oheimb 1996-12-13 adaptions for symbol font
1996-11-27 wenzelm 1996-11-27 moved "1", "2" to syntax section;
1996-06-25 berghofe 1996-06-25 Changed argument order of nat_rec.
1996-04-23 oheimb 1996-04-23 *** empty log message ***
1996-04-23 oheimb 1996-04-23 repaired critical proofs depending on the order inside non-confluent SimpSets, (temporarily) removed problematic rule less_Suc_eq form simpset_of "Nat"
1996-04-17 oheimb 1996-04-17 *** empty log message ***
1996-03-28 paulson 1996-03-28 Translations for 1 and 2 moved from Hoare/Examples.thy to Nat.thy
1996-03-05 paulson 1996-03-05 Converted TABs to spaces
1996-03-04 nipkow 1996-03-04 Added a constant UNIV == {x.True} Added many new rewrite rules for sets. Moved LEAST into Nat. Added cardinality to Finite.
1996-02-05 clasohm 1996-02-05 expanded tabs; renamed subtype to typedef; incorporated Konrad's changes
1995-11-29 clasohm 1995-11-29 removed quotes from types in consts and syntax sections
1995-06-21 clasohm 1995-06-21 removed \...\ inside strings
1995-03-24 clasohm 1995-03-24 changed syntax of tuples from <..., ...> to (..., ...)
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application