src/HOL/Nat.thy
2012-09-15 haftmann 2012-09-15 typeclass formalising bounded subtraction
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-07-27 huffman 2012-07-27 replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
2012-07-27 huffman 2012-07-27 give Nat_Arith simprocs proper name bindings by using simproc_setup
2012-05-24 wenzelm 2012-05-24 tuned proofs;
2012-04-16 huffman 2012-04-16 tuned some proofs; removed duplicate lemma zero_le_imp_of_nat
2012-04-01 huffman 2012-04-01 removed Nat_Numeral.thy, moving all theorems elsewhere
2012-03-30 huffman 2012-03-30 move lemmas from Nat_Numeral.thy to Nat.thy
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-01-28 bulwahn 2012-01-28 adding yet another induction rule on natural numbers
2012-01-28 bulwahn 2012-01-28 moving declarations back to the section they seem to belong to (cf. afffe1f72143)
2011-12-29 haftmann 2011-12-29 attribute code_abbrev superseedes code_unfold_post
2011-12-24 haftmann 2011-12-24 generalized type signature to permit overloading on `set`
2011-12-19 noschinl 2011-12-19 add lemmas
2011-12-19 noschinl 2011-12-19 weaken preconditions on lemmas
2011-12-13 nipkow 2011-12-13 lemmas about Kleene iteration
2011-11-30 wenzelm 2011-11-30 prefer typedef without alternative name;
2011-10-21 bulwahn 2011-10-21 replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-09-08 huffman 2011-09-08 remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
2011-09-07 haftmann 2011-09-07 lemmas about +, *, min, max on nat
2011-08-20 haftmann 2011-08-20 more uniform formatting of specifications
2011-08-18 haftmann 2011-08-18 observe distinction between sets and predicates more properly
2011-06-29 wenzelm 2011-06-29 modernized some simproc setup;
2010-09-30 haftmann 2010-09-30 tuned
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-08-20 haftmann 2010-08-20 more concise characterization of of_nat operation and class semiring_char_0
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-06-14 haftmann 2010-06-14 added lemma funpow_mult
2010-06-08 haftmann 2010-06-08 qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
2010-05-17 huffman 2010-05-17 declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-03-18 blanchet 2010-03-18 now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
2010-03-07 huffman 2010-03-07 add lemmas Nats_cases and Nats_induct
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-02-18 huffman 2010-02-18 get rid of many duplicate simp rule warnings
2010-02-12 haftmann 2010-02-12 tuned import order
2010-02-09 haftmann 2010-02-09 hide fact names clashing with fact names from Group.thy
2010-02-08 haftmann 2010-02-08 hide fact Nat.add_0_right; make add_0_right from Groups priority
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2009-12-30 krauss 2009-12-30 more regular axiom of infinity, with no (indirect) reference to overloaded constants
2009-11-13 nipkow 2009-11-13 renamed lemmas "anti_sym" -> "antisym"
2009-10-30 haftmann 2009-10-30 tuned code setup
2009-10-28 haftmann 2009-10-28 moved lemmas for dvd on nat to theories Nat and Power
2009-09-30 haftmann 2009-09-30 tuned whitespace
2009-08-31 nipkow 2009-08-31 tuned the simp rules for Int involving insert and intervals.
2009-08-28 nipkow 2009-08-28 tuned proofs
2009-07-14 haftmann 2009-07-14 code attributes use common underscore convention
2009-06-18 krauss 2009-06-18 generalized less_Suc_induct
2009-05-14 haftmann 2009-05-14 monomorphic code generation for power operations
2009-05-11 haftmann 2009-05-11 tuned interface of Lin_Arith
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.