src/HOL/Nat.thy
2014-08-16 wenzelm 2014-08-16 updated to named_theorems;
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-11 Thomas Sewell 2014-06-11 Hypsubst preserves equality hypotheses Fixes included for various theories affected by this change.
2014-06-10 blanchet 2014-06-10 use 'where' clause for selector default value syntax
2014-05-26 blanchet 2014-05-26 got rid of '=:' squiggly
2014-05-20 nipkow 2014-05-20 added lemma
2014-03-18 hoelzl 2014-03-18 fix HOL-NSA; move lemmas
2014-03-10 hoelzl 2014-03-10 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
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;