src/HOL/Nat.thy
2008-08-11 haftmann 2008-08-11 moved class wellorder to theory Orderings
2008-08-08 nipkow 2008-08-08 added lemmas
2008-07-25 haftmann 2008-07-25 tuned
2008-07-17 krauss 2008-07-17 simplified proofs
2008-07-17 nipkow 2008-07-17 added lemmas
2008-06-14 wenzelm 2008-06-14 removed obsolete nat_induct_tac -- cannot work without;
2008-06-10 wenzelm 2008-06-10 added nat_induct_tac (works without context);
2008-06-10 haftmann 2008-06-10 rep_datatype command now takes list of constructors as input arguments
2008-04-25 krauss 2008-04-25 Merged theories about wellfoundedness into one: Wellfounded.thy
2008-03-19 wenzelm 2008-03-19 removed redundant Nat.less_not_sym, Nat.less_asym; renamed Nat.less_irrefl to less_irrefl_nat, no longer declared elim;
2008-03-18 wenzelm 2008-03-18 removed redundant less_trans, less_linear, le_imp_less_or_eq, le_less_trans, less_le_trans (cf. Orderings.thy); renamed less_imp_le to less_imp_le_nat;
2008-03-17 wenzelm 2008-03-17 removed duplicate lemmas;
2008-02-26 haftmann 2008-02-26 tuned heading
2008-02-26 bulwahn 2008-02-26 Added useful general lemmas from the work with the HeapMonad
2008-02-20 haftmann 2008-02-20 tuned structures in arith_data.ML
2008-02-15 haftmann 2008-02-15 <= and < on nat no longer depend on wellfounded relations
2008-01-21 haftmann 2008-01-21 tuned code setup
2007-12-18 berghofe 2007-12-18 Renamed *.size to prod.size.
2007-12-13 haftmann 2007-12-13 added lemma
2007-12-07 haftmann 2007-12-07 instantiation target rather than legacy instance
2007-12-06 haftmann 2007-12-06 temporary code generator work arounds
2007-12-06 haftmann 2007-12-06 authentic primrec
2007-12-05 haftmann 2007-12-05 simplified infrastructure for code generator operational equality
2007-11-30 haftmann 2007-11-30 adjustions to due to instance target
2007-11-29 haftmann 2007-11-29 instance command as rudimentary class target
2007-11-28 haftmann 2007-11-28 dropped implicit assumption proof
2007-11-10 wenzelm 2007-11-10 tuned specifications of 'notation';
2007-10-30 haftmann 2007-10-30 simplified proof
2007-10-25 haftmann 2007-10-25 various localizations
2007-10-23 nipkow 2007-10-23 went back to >0
2007-10-23 paulson 2007-10-23 random tidying of proofs
2007-10-22 haftmann 2007-10-22 dropped superfluous inlining lemmas
2007-10-21 nipkow 2007-10-21 More changes from >0 to ~=0::nat
2007-10-21 nipkow 2007-10-21 Eliminated most of the neq0_conv occurrences. As a result, many theorems had to be rephrased with ~= 0 instead of > 0.
2007-10-20 chaieb 2007-10-20 neq0_conv removed from [iff] -- causes problems by simple goals with blast, auto etc...
2007-10-18 haftmann 2007-10-18 localized mono predicate
2007-10-16 haftmann 2007-10-16 global class syntax
2007-10-12 haftmann 2007-10-12 refined; moved class power to theory Power
2007-09-26 haftmann 2007-09-26 added code lemma for 1
2007-09-25 haftmann 2007-09-25 datatype interpretators for size and datatype_realizer
2007-09-03 nipkow 2007-09-03 added variations on infinite descent
2007-08-27 nipkow 2007-08-27 Added infinite_descent
2007-08-15 paulson 2007-08-15 ATP blacklisting is now in theory data, attribute noatp
2007-08-09 haftmann 2007-08-09 localized of_nat
2007-08-07 haftmann 2007-08-07 split off theory Option for benefit of code generator
2007-07-31 wenzelm 2007-07-31 added Tools/lin_arith.ML;
2007-07-31 wenzelm 2007-07-31 arith method setup: proper context;
2007-07-19 haftmann 2007-07-19 moved set Nats to Nat.thy
2007-07-11 berghofe 2007-07-11 Adapted to new package for inductive sets.
2007-06-22 huffman 2007-06-22 fix looping simp rule
2007-06-20 huffman 2007-06-20 remove simp attribute from of_nat_diff, for backward compatibility with zdiff_int
2007-06-20 huffman 2007-06-20 change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
2007-06-12 huffman 2007-06-12 add lemma inj_of_nat
2007-06-06 huffman 2007-06-06 add axclass semiring_char_0 for types where of_nat is injective
2007-06-06 huffman 2007-06-06 generalize of_nat and related constants to class semiring_1
2007-06-05 haftmann 2007-06-05 tuned boostrap
2007-05-17 krauss 2007-05-17 added induction principles for induction "backwards": P (Suc n) ==> P n
2007-05-10 haftmann 2007-05-10 size [nat] is identity
2007-05-06 haftmann 2007-05-06 changed code generator invocation syntax
2007-04-20 haftmann 2007-04-20 Isar definitions are now added explicitly to code theorem table