src/HOL/Nat.thy
2016-02-19 hoelzl 2016-02-19 generalize more theorems to support enat and ennreal
2016-02-10 hoelzl 2016-02-10 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 haftmann 2016-02-18 sorted out some duplicate fact bindings
2016-02-17 haftmann 2016-02-17 pulled out legacy aliasses and infamous dvd interpretations into theory appendix
2016-02-17 blanchet 2016-02-17 allow predicator instead of map function in 'primrec'
2016-01-22 paulson 2016-01-22 Reorganised a huge proof
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-13 paulson 2015-11-13 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-11-02 eberlm 2015-11-02 Rounding function, uniform limits, cotangent, binomial identities
2015-10-09 wenzelm 2015-10-09 discontinued specific HTML syntax;
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-09-09 wenzelm 2015-09-09 simplified simproc programming interfaces;
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
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