src/HOL/Nat.thy
2014-02-21 blanchet 2014-02-21 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
2014-02-19 blanchet 2014-02-19 moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
2014-02-17 blanchet 2014-02-17 renamed old 'primrec' to 'old_primrec' (until the new 'primrec' can be moved above 'Nat' in the theory dependencies)
2014-02-14 blanchet 2014-02-14 aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
2014-02-14 blanchet 2014-02-14 renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)
2014-02-12 blanchet 2014-02-12 don't hide constant forever, since it may appear in some 'primcorec'-generated theorems
2014-02-12 blanchet 2014-02-12 remove hidden fact about hidden constant from code generator setup
2014-02-12 blanchet 2014-02-12 for extraction -- use the exhaust rule that's registered with 'datatype_realizer.ML'
2014-02-12 blanchet 2014-02-12 adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'
2014-02-12 blanchet 2014-02-12 renamed 'nat_{case,rec}' to '{case,rec}_nat'
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-11-18 hoelzl 2013-11-18 add lemmas Suc_funpow and id_funpow to simpset; add lemma map_add_upt
2013-11-12 hoelzl 2013-11-12 stronger inc_induct and dec_induct
2013-10-31 haftmann 2013-10-31 restructed
2013-10-31 haftmann 2013-10-31 generalised lemma
2013-10-18 blanchet 2013-10-18 killed most "no_atp", to make Sledgehammer more complete
2013-09-29 haftmann 2013-09-29 tuned proofs
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-07-25 haftmann 2013-07-25 factored syntactic type classes for bot and top (by Alessandro Coglio)
2013-06-23 haftmann 2013-06-23 migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
2013-06-02 haftmann 2013-06-02 type class for confined subtraction
2013-02-20 hoelzl 2013-02-20 split dense into inner_dense_order and no_top/no_bot
2013-02-24 haftmann 2013-02-24 turned example into library for comparing growth of functions
2013-02-17 haftmann 2013-02-17 Sieve of Eratosthenes
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-10-06 haftmann 2012-10-06 alternative simplification of ^^ to the righthand side; lifting of comp_fun_commute to ^^
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;