src/HOL/Nat.thy
2016-05-23 ago removed odd cases rule (see also 8cb42cd97579);
2016-05-23 ago tuned document;
2016-05-23 ago misc tuning and modernization;
2016-05-17 ago Moved material from AFP/Randomised_Social_Choice to distribution
2016-04-25 ago eliminated old 'def';
2016-03-21 ago clarified rule structure;
2016-03-13 ago more theorems on orderings
2016-03-03 ago removed junk;
2016-03-01 ago tuned bootstrap order to provide type classes in a more sensible order
2016-02-19 ago generalize more theorems to support enat and ennreal
2016-02-10 ago Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
2016-02-18 ago sorted out some duplicate fact bindings
2016-02-17 ago pulled out legacy aliasses and infamous dvd interpretations into theory appendix
2016-02-17 ago allow predicator instead of map function in 'primrec'
2016-01-22 ago Reorganised a huge proof
2015-12-07 ago isabelle update_cartouches -c -t;
2015-11-13 ago Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-11-02 ago Rounding function, uniform limits, cotangent, binomial identities
2015-10-09 ago discontinued specific HTML syntax;
2015-09-13 ago tuned proofs -- less legacy;
2015-09-09 ago simplified simproc programming interfaces;
2015-09-01 ago eliminated \<Colon>;
2015-08-31 ago prefer symbols;
2015-07-18 ago isabelle update_cartouches;
2015-07-03 ago add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
2015-06-23 ago 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 ago add transfer theorems for fixed points
2015-06-01 ago implicit partial divison operation in integral domains
2015-05-05 ago add lfp/gfp rule for nn_integral
2015-03-28 ago clarified no_zero_devisors: makes only sense in a semiring;
2015-03-23 ago distributivity of partial minus establishes desired properties of dvd in semirings
2015-03-23 ago explicit commutative additive inverse operation;
2015-03-04 ago tuned signature -- prefer qualified names;
2014-11-13 ago import general theorems from AFP/Markov_Models
2014-11-08 ago equivalence rules for structures without zero divisors
2014-11-02 ago modernized header uniformly as section;
2014-10-29 ago modernized setup;
2014-10-12 ago generalized and consolidated some theorems concerning divisibility
2014-10-12 ago more facts about abstract divisibility
2014-09-19 ago made new 'primrec' bootstrapping-capable
2014-09-18 ago moved old 'size' generator together with 'old_datatype'
2014-09-11 ago renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
2014-09-05 ago added 'plugins' option to control which hooks are enabled
2014-08-18 ago reordered some (co)datatype property names for more consistency
2014-08-16 ago updated to named_theorems;
2014-07-05 ago prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 ago reduced name variants for assoc and commute on plus and mult
2014-06-11 ago Hypsubst preserves equality hypotheses
2014-06-10 ago use 'where' clause for selector default value syntax
2014-05-26 ago got rid of '=:' squiggly
2014-05-20 ago added lemma
2014-03-18 ago fix HOL-NSA; move lemmas
2014-03-10 ago 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 ago adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
2014-02-19 ago moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
2014-02-17 ago renamed old 'primrec' to 'old_primrec' (until the new 'primrec' can be moved above 'Nat' in the theory dependencies)
2014-02-14 ago aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
2014-02-14 ago renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)
2014-02-12 ago don't hide constant forever, since it may appear in some 'primcorec'-generated theorems
2014-02-12 ago remove hidden fact about hidden constant from code generator setup