src/HOL/NthRoot.thy
Tue, 17 Sep 2019 16:21:31 +0100 paulson A couple of new theorems, stolen from AFP entries
Thu, 18 Jul 2019 14:08:28 +0100 paulson more new material about analysis
Wed, 17 Jul 2019 14:02:42 +0100 paulson a few new lemmas and a bit of tidying
Tue, 10 Jul 2018 23:18:08 +0100 paulson de-applying, etc.
Mon, 18 Jun 2018 14:22:26 +0100 paulson New material in support of quaternions
Thu, 03 May 2018 22:34:49 +0100 paulson Some tidying up (mostly regarding summations from 0)
Thu, 22 Feb 2018 15:17:25 +0100 immler moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
Sun, 08 Oct 2017 22:28:22 +0200 haftmann one uniform type class for parity structures
Sat, 22 Apr 2017 22:01:35 +0200 wenzelm theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
Mon, 17 Oct 2016 11:46:22 +0200 nipkow setsum -> sum
Mon, 10 Oct 2016 15:45:41 +0100 paulson invariance of domain
Thu, 25 Aug 2016 15:50:43 +0200 Manuel Eberl More analysis lemmas
Thu, 28 Jul 2016 20:39:46 +0200 wenzelm misc tuning and modernization;
Tue, 12 Jul 2016 22:54:37 +0200 wenzelm misc tuning and modernization;
Sat, 09 Jul 2016 13:26:16 +0200 haftmann more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
Sat, 02 Jul 2016 20:22:25 +0200 haftmann simplified definitions of combinatorial functions
Mon, 25 Apr 2016 16:09:26 +0200 wenzelm eliminated old 'def';
Tue, 23 Feb 2016 18:04:31 +0100 nipkow resolved conflict
Tue, 23 Feb 2016 16:25:08 +0100 nipkow more canonical names
Tue, 23 Feb 2016 15:47:39 +0000 paulson New and revised material for (multivariate) analysis
Wed, 17 Feb 2016 21:51:57 +0100 haftmann generalized some lemmas;
Mon, 11 Jan 2016 22:14:15 +0000 paulson nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
Wed, 30 Dec 2015 11:21:54 +0100 wenzelm more symbols;
Tue, 29 Dec 2015 23:04:53 +0100 wenzelm more symbols;
Mon, 28 Dec 2015 01:26:34 +0100 wenzelm prefer symbols for "abs";
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.
Tue, 10 Nov 2015 14:18:41 +0000 paulson Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
Thu, 06 Aug 2015 23:56:48 +0200 haftmann slight cleanup of lemmas
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Tue, 30 Jun 2015 13:56:16 +0100 paulson Useful lemmas. The theorem concerning swapping the variables in a double integral.
Tue, 21 Apr 2015 17:19:00 +0100 paulson New material, mostly about limits. Consolidation.
Wed, 18 Mar 2015 14:13:27 +0000 paulson Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Thu, 23 Oct 2014 14:04:05 +0200 haftmann downshift of theory Parity in the hierarchy
Sun, 19 Oct 2014 18:05:26 +0200 haftmann prefer generic elimination rules for even/odd over specialized unfold rules for nat
Sat, 05 Jul 2014 11:01:53 +0200 haftmann prefer ac_simps collections over separate name bindings for add and mult
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
Wed, 18 Jun 2014 07:31:12 +0200 hoelzl moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
Mon, 02 Jun 2014 16:19:37 +0200 hoelzl remove superfluous assumption
Wed, 07 May 2014 12:25:35 +0200 hoelzl avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
Fri, 11 Apr 2014 13:36:57 +0200 nipkow made mult_nonneg_nonneg a simp rule
Thu, 03 Apr 2014 17:56:08 +0200 hoelzl merged DERIV_intros, has_derivative_intros into derivative_intros
Wed, 02 Apr 2014 18:35:07 +0200 hoelzl extend continuous_intros; remove continuous_on_intros and isCont_intros
Fri, 07 Mar 2014 12:35:06 +0000 paulson a few new lemmas
Tue, 12 Nov 2013 19:28:54 +0100 hoelzl add finite_select_induct; move generic lemmas from MV_Analysis/Linear_Algebra to the HOL image
Thu, 12 Sep 2013 09:04:46 -0700 huffman prefer attribute 'unfolded thm' to 'simplified'
Sun, 18 Aug 2013 18:49:45 +0200 wenzelm more symbols;
Tue, 13 Aug 2013 16:25:47 +0200 wenzelm standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl modernized definition of root: use the_inv, handle positive and negative case uniformly, and 0-th root is constant 0
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
Fri, 19 Oct 2012 15:12:52 +0200 webertj Renamed {left,right}_distrib to distrib_{right,left}.
Wed, 10 Oct 2012 15:17:40 +0200 wenzelm eliminated spurious fact duplicates;
Sat, 20 Aug 2011 15:54:26 -0700 huffman remove redundant lemma real_0_le_divide_iff in favor or zero_le_divide_iff
Fri, 19 Aug 2011 19:01:00 -0700 huffman remove some redundant simp rules about sqrt
Thu, 18 Aug 2011 19:53:03 -0700 huffman optimize some proofs
Thu, 18 Feb 2010 14:21:44 -0800 huffman get rid of many duplicate simp rule warnings
Tue, 30 Jun 2009 18:16:22 +0200 hoelzl Added DERIV_intros
Tue, 28 Apr 2009 15:50:29 +0200 haftmann collected square lemmas in Nat_Numeral
Wed, 04 Mar 2009 17:12:23 -0800 huffman declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
Wed, 03 Dec 2008 15:58:44 +0100 haftmann made repository layout more coherent with logical distribution structure; stripped some $Id$s
less more (0) tip