src/HOL/Nat.thy
2015-08-31 wenzelm 2015-08-31 prefer symbols;
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-07-03 hoelzl 2015-07-03 add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
2015-06-23 paulson 2015-06-23 Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
2015-06-11 hoelzl 2015-06-11 add transfer theorems for fixed points
2015-06-01 haftmann 2015-06-01 implicit partial divison operation in integral domains
2015-05-05 hoelzl 2015-05-05 add lfp/gfp rule for nn_integral
2015-03-28 haftmann 2015-03-28 clarified no_zero_devisors: makes only sense in a semiring; actually turn linorder_semidom into a integral domain
2015-03-23 haftmann 2015-03-23 distributivity of partial minus establishes desired properties of dvd in semirings
2015-03-23 haftmann 2015-03-23 explicit commutative additive inverse operation; more explicit focal point for commutative monoids with an inverse operation
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2014-11-13 hoelzl 2014-11-13 import general theorems from AFP/Markov_Models
2014-11-08 haftmann 2014-11-08 equivalence rules for structures without zero divisors
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-10-12 haftmann 2014-10-12 generalized and consolidated some theorems concerning divisibility
2014-10-12 haftmann 2014-10-12 more facts about abstract divisibility
2014-09-19 blanchet 2014-09-19 made new 'primrec' bootstrapping-capable
2014-09-18 blanchet 2014-09-18 moved old 'size' generator together with 'old_datatype'
2014-09-11 blanchet 2014-09-11 renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
2014-09-05 blanchet 2014-09-05 added 'plugins' option to control which hooks are enabled
2014-08-18 blanchet 2014-08-18 reordered some (co)datatype property names for more consistency
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;