src/HOL/Nat.thy
2009-04-29 huffman 2009-04-29 reimplement reorientation simproc using theory data
2009-04-24 haftmann 2009-04-24 some jokes are just too bad to appear in a theory file
2009-04-24 haftmann 2009-04-24 funpow and relpow with shared "^^" syntax
2009-04-23 haftmann 2009-04-23 avoid local [code]
2009-04-20 haftmann 2009-04-20 power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
2009-03-23 haftmann 2009-03-23 moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
2009-03-12 haftmann 2009-03-12 vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-02-26 huffman 2009-02-26 revert some Suc 0 lemmas back to their original forms; added some simp rules for (1::nat)
2009-02-25 huffman 2009-02-25 add lemma diff_Suc_1
2009-02-23 huffman 2009-02-23 make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
2009-02-22 nipkow 2009-02-22 added lemmas
2009-02-12 nipkow 2009-02-12 Moved FTA into Lib and cleaned it up a little.
2009-02-10 paulson 2009-02-10 merged
2009-02-10 paulson 2009-02-10 Deleted the induction rule nat_induct2, which was too weak and not used even once.
2009-02-09 nipkow 2009-02-09 new attribute "arith" for facts supplied to arith.
2009-01-28 nipkow 2009-01-28 merged - resolving conflics
2009-01-28 nipkow 2009-01-28 Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now
2009-01-28 haftmann 2009-01-28 nat is a bot instance
2009-01-21 haftmann 2009-01-21 no base sort in class import
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s
2008-11-17 haftmann 2008-11-17 tuned unfold_locales invocation
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-10-07 haftmann 2008-10-07 tuned of_nat code generation
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...