src/HOL/Nat.thy
Thu, 14 May 2020 23:44:01 +0200 nipkow added lemma
Mon, 04 May 2020 17:35:29 +0200 Manuel Eberl New HOL simproc 'datatype_no_proper_subterm'
Mon, 23 Mar 2020 10:25:56 +0000 paulson put back Nat.le_diff_conv2 because AUTO2 doesn't work with Groups.le_diff_conv2
Sun, 22 Mar 2020 17:21:16 +0000 paulson tidying up some horrible proofs
Sun, 09 Feb 2020 21:58:42 +0000 haftmann more rules for natural deduction from inequalities
Sun, 26 Jan 2020 20:35:31 +0000 haftmann generalized
Mon, 27 Jan 2020 14:32:43 +0000 paulson A few lemmas connected with orderings
Thu, 08 Aug 2019 12:11:40 +0200 wenzelm prefer named lemmas -- more compact proofterms;
Wed, 17 Jul 2019 14:02:42 +0100 paulson a few new lemmas and a bit of tidying
Sat, 22 Jun 2019 07:18:55 +0000 haftmann streamlined setup for linear algebra, particularly removed redundant rule declarations
Mon, 21 Jan 2019 14:44:23 +0000 paulson new material about summations and powers, along with some tweaks
Mon, 14 Jan 2019 18:35:03 +0000 haftmann tuned proofs
Sun, 06 Jan 2019 15:04:34 +0100 wenzelm isabelle update -u path_cartouches;
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Thu, 12 Jul 2018 17:22:39 +0100 paulson de-applying (mostly Set_Interval)
Wed, 11 Jul 2018 01:04:23 +0200 nipkow moved lemmas
Fri, 23 Feb 2018 09:28:14 +0000 paulson fixing ennreal using add_mono1; shifting results from linordered_semidom to linordered_nonzero_semiring
Mon, 19 Feb 2018 16:44:45 +0000 paulson lots of new material, ultimately related to measure theory
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Wed, 03 Jan 2018 11:06:13 +0100 blanchet kill old size infrastructure
Sun, 26 Nov 2017 21:08:32 +0100 wenzelm more symbols;
Sat, 11 Nov 2017 18:33:35 +0000 haftmann more induct rules on nat
Mon, 30 Oct 2017 19:29:06 +0000 haftmann added lemma
Mon, 30 Oct 2017 13:18:41 +0000 haftmann tuned some proofs and added some lemmas
Sun, 08 Oct 2017 22:28:22 +0200 haftmann more fundamental definition of div and mod on int
Sun, 08 Oct 2017 22:28:21 +0200 haftmann generalized simproc
Wed, 09 Aug 2017 12:01:16 +0200 nipkow added lemmas
Wed, 26 Jul 2017 13:36:36 +0100 paulson moved transitive_stepwise_le into Nat, where it belongs
Thu, 20 Jul 2017 16:28:43 +0100 blanchet strengthened tactic
Tue, 30 May 2017 14:04:48 +0200 nipkow tuned names
Tue, 30 May 2017 10:03:35 +0200 nipkow redefined Greatest
Wed, 26 Apr 2017 15:53:35 +0100 paulson Further new material. The simprule status of some exp and ln identities was reverted.
Wed, 11 Jan 2017 16:43:31 +0100 blanchet generalized types in lemmas
Mon, 09 Jan 2017 18:53:20 +0100 haftmann moved some lemmas to appropriate places
Fri, 30 Dec 2016 18:02:27 +0100 haftmann dropped slightly outdated comment
Tue, 22 Nov 2016 18:36:59 +0100 nipkow added lemma
Sat, 01 Oct 2016 17:16:35 +0200 wenzelm clarified lfp/gfp statements and proofs;
Wed, 10 Aug 2016 09:33:54 +0200 nipkow "split add" -> "split"
Tue, 02 Aug 2016 21:05:34 +0200 wenzelm misc tuning and modernization;
Fri, 29 Jul 2016 09:49:23 +0200 Andreas Lochbihler add lemmas contributed by Peter Gammie
Tue, 31 May 2016 19:51:01 +0200 wenzelm rat.ML is now part of Pure to allow tigther integration with Isabelle/ML;
Wed, 25 May 2016 11:49:40 +0200 wenzelm isabelle update_cartouches -c -t;
Mon, 23 May 2016 15:30:13 +0200 wenzelm removed odd cases rule (see also 8cb42cd97579);
Mon, 23 May 2016 14:56:48 +0200 wenzelm tuned document;
Mon, 23 May 2016 14:43:14 +0200 wenzelm misc tuning and modernization;
Tue, 17 May 2016 17:05:35 +0200 eberlm Moved material from AFP/Randomised_Social_Choice to distribution
Mon, 25 Apr 2016 16:09:26 +0200 wenzelm eliminated old 'def';
Mon, 21 Mar 2016 21:18:08 +0100 wenzelm clarified rule structure;
Sun, 13 Mar 2016 10:22:46 +0100 haftmann more theorems on orderings
Thu, 03 Mar 2016 11:54:51 +0100 wenzelm removed junk;
Tue, 01 Mar 2016 10:36:19 +0100 haftmann tuned bootstrap order to provide type classes in a more sensible order
Fri, 19 Feb 2016 13:40:50 +0100 hoelzl generalize more theorems to support enat and ennreal
Wed, 10 Feb 2016 18:43:19 +0100 hoelzl 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.
Thu, 18 Feb 2016 17:52:53 +0100 haftmann sorted out some duplicate fact bindings
Wed, 17 Feb 2016 21:51:56 +0100 haftmann pulled out legacy aliasses and infamous dvd interpretations into theory appendix
Wed, 17 Feb 2016 11:54:34 +0100 blanchet allow predicator instead of map function in 'primrec'
Fri, 22 Jan 2016 16:00:03 +0000 paulson Reorganised a huge proof
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Fri, 13 Nov 2015 12:27:13 +0000 paulson Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
Mon, 02 Nov 2015 11:56:28 +0100 eberlm Rounding function, uniform limits, cotangent, binomial identities
less more (0) -300 -100 -60 tip