src/HOL/Nat.thy
19 months ago haftmann 2017-10-30 added lemma
19 months ago haftmann 2017-10-30 tuned some proofs and added some lemmas
20 months ago haftmann 2017-10-08 more fundamental definition of div and mod on int
20 months ago haftmann 2017-10-08 generalized simproc
22 months ago nipkow 2017-08-09 added lemmas
23 months ago paulson 2017-07-26 moved transitive_stepwise_le into Nat, where it belongs
23 months ago blanchet 2017-07-20 strengthened tactic
2017-05-30 nipkow 2017-05-30 tuned names
2017-05-30 nipkow 2017-05-30 redefined Greatest
2017-04-26 paulson 2017-04-26 Further new material. The simprule status of some exp and ln identities was reverted.
2017-01-11 blanchet 2017-01-11 generalized types in lemmas
2017-01-09 haftmann 2017-01-09 moved some lemmas to appropriate places
2016-12-30 haftmann 2016-12-30 dropped slightly outdated comment
2016-11-22 nipkow 2016-11-22 added lemma
2016-10-01 wenzelm 2016-10-01 clarified lfp/gfp statements and proofs;
2016-08-10 nipkow 2016-08-10 "split add" -> "split"
2016-08-02 wenzelm 2016-08-02 misc tuning and modernization;
2016-07-29 Andreas Lochbihler 2016-07-29 add lemmas contributed by Peter Gammie
2016-05-31 wenzelm 2016-05-31 rat.ML is now part of Pure to allow tigther integration with Isabelle/ML;
2016-05-25 wenzelm 2016-05-25 isabelle update_cartouches -c -t;
2016-05-23 wenzelm 2016-05-23 removed odd cases rule (see also 8cb42cd97579);
2016-05-23 wenzelm 2016-05-23 tuned document;
2016-05-23 wenzelm 2016-05-23 misc tuning and modernization;
2016-05-17 eberlm 2016-05-17 Moved material from AFP/Randomised_Social_Choice to distribution
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-03-21 wenzelm 2016-03-21 clarified rule structure;
2016-03-13 haftmann 2016-03-13 more theorems on orderings
2016-03-03 wenzelm 2016-03-03 removed junk;
2016-03-01 haftmann 2016-03-01 tuned bootstrap order to provide type classes in a more sensible order
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