src/HOL/Multivariate_Analysis/Integration.thy
Wed, 15 Jun 2016 15:52:24 +0100 paulson Urysohn's lemma, Dugundji extension theorem and many other proofs
Tue, 14 Jun 2016 15:54:28 +0100 paulson Merge
Tue, 14 Jun 2016 15:34:21 +0100 paulson new results about topology
Tue, 14 Jun 2016 13:14:11 +0200 eberlm Integration by substitution
Mon, 13 Jun 2016 17:39:52 +0200 eberlm Integral form of Gamma function
Mon, 13 Jun 2016 15:23:12 +0200 eberlm Facts about HK integration, complex powers, Gamma function
Fri, 27 May 2016 20:23:55 +0200 wenzelm tuned proofs, to allow unfold_abs_def;
Fri, 13 May 2016 20:24:10 +0200 wenzelm eliminated use of empty "assms";
Mon, 25 Apr 2016 16:09:26 +0200 wenzelm eliminated old 'def';
Mon, 18 Apr 2016 16:50:19 +0100 paulson tidying some proofs; getting rid of "nonempty_witness"
Mon, 18 Apr 2016 14:30:32 +0100 paulson new theorems about convex hulls, etc.; also, renamed some theorems
Sun, 03 Apr 2016 23:03:30 +0200 wenzelm isabelle update_cartouches -c -t;
Wed, 16 Mar 2016 13:57:06 +0000 paulson Contractible sets. Also removal of obsolete theorems and refactoring
Tue, 15 Mar 2016 14:08:25 +0000 paulson rationalisation of theorem names esp about "real Archimedian" etc.
Mon, 14 Mar 2016 14:19:06 +0000 paulson Refactoring (moving theorems into better locations), plus a bit of new material
Mon, 07 Mar 2016 14:34:45 +0000 paulson new material to Blochj's theorem, as well as supporting lemmas
Mon, 29 Feb 2016 11:42:15 +0000 paulson the integral is 0 when otherwise it would be undefined (also for contour integrals)
Tue, 23 Feb 2016 16:25:08 +0100 nipkow more canonical names
Wed, 17 Feb 2016 21:51:56 +0100 haftmann prefer abbreviations for compound operators INFIMUM and SUPREMUM
Wed, 20 Jan 2016 13:16:58 +0100 immler added lemma
Fri, 15 Jan 2016 10:14:31 +0100 immler continuity of parameterized integral; easier-to-apply formulation of rules
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:28:28 +0100 wenzelm more symbols;
Tue, 22 Dec 2015 21:58:27 +0100 immler theory for type of bounded linear functions; differentiation under the integral sign
Thu, 10 Dec 2015 13:38:40 +0000 paulson not_leE -> not_le_imp_less and other tidying
Wed, 09 Dec 2015 17:35:22 +0000 paulson sorted out eventually_mono
Mon, 07 Dec 2015 20:19:59 +0100 wenzelm isabelle update_cartouches -c -t;
Mon, 07 Dec 2015 16:44:26 +0000 paulson Cauchy's integral formula for circles. Starting to fix eventually_mono.
Tue, 01 Dec 2015 14:09:10 +0000 paulson Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
Sun, 22 Nov 2015 23:19:43 +0100 wenzelm more symbols;
Fri, 13 Nov 2015 20:03:27 +0100 wenzelm merged
Fri, 13 Nov 2015 17:48:33 +0100 wenzelm preserve names of for-fixes for faithfully;
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, 29 Oct 2015 15:40:52 +0100 eberlm added many small lemmas about setsum/setprod/powr/...
Mon, 26 Oct 2015 23:41:27 +0000 paulson new lemmas about topology, etc., for Cauchy integral formula
Tue, 13 Oct 2015 09:21:15 +0200 haftmann prod_case as canonical name for product type eliminator
Thu, 24 Sep 2015 14:29:08 +0200 immler exchange uniform limit and integral
Mon, 21 Sep 2015 21:46:14 +0200 wenzelm isabelle update_cartouches;
Mon, 21 Sep 2015 19:52:13 +0100 paulson new lemmas and movement of lemmas into place
Sun, 13 Sep 2015 21:06:58 +0200 wenzelm tuned proofs;
Sun, 13 Sep 2015 20:20:16 +0200 wenzelm renamed method "goals" to "goal_cases" to emphasize its meaning;
Sun, 13 Sep 2015 16:50:12 +0200 wenzelm tuned proofs;
Tue, 01 Sep 2015 22:32:58 +0200 wenzelm eliminated \<Colon>;
Thu, 06 Aug 2015 23:56:48 +0200 haftmann slight cleanup of lemmas
Tue, 28 Jul 2015 17:15:01 +0100 paulson tweaks. Got rid of a really slow step
Mon, 27 Jul 2015 16:52:57 +0100 paulson New material for Cauchy's integral theorem
Mon, 20 Jul 2015 23:12:50 +0100 paulson new material for multivariate analysis, etc.
Wed, 01 Jul 2015 13:09:56 +0200 immler taylor series with has_integral and integrable_on
Tue, 30 Jun 2015 13:56:16 +0100 paulson Useful lemmas. The theorem concerning swapping the variables in a double integral.
Fri, 26 Jun 2015 10:20:33 +0200 wenzelm tuned whitespace;
Tue, 16 Jun 2015 20:50:00 +0100 paulson another messy proof fixed
Mon, 15 Jun 2015 21:33:26 +0100 paulson inverted another messy proof
Sun, 14 Jun 2015 18:51:34 +0100 paulson another tangled proof
Sun, 14 Jun 2015 17:05:27 +0100 paulson Tidied up more proofs
Sun, 14 Jun 2015 14:25:01 +0100 paulson another proof
Sun, 14 Jun 2015 12:48:32 +0100 paulson fixing more proofs
Sat, 13 Jun 2015 22:48:47 +0100 paulson fixed another horrible proof
Sat, 13 Jun 2015 19:23:41 +0100 paulson streamlined many more proofs
less more (0) -100 -60 tip