| Sat, 02 Jul 2016 20:22:25 +0200 |
haftmann |
simplified definitions of combinatorial functions
|
file |
diff |
annotate
|
| Thu, 09 Jun 2016 16:11:33 +0200 |
hoelzl |
remove smt call in Lebesge_Measure
|
file |
diff |
annotate
|
| Fri, 13 May 2016 20:24:10 +0200 |
wenzelm |
eliminated use of empty "assms";
|
file |
diff |
annotate
|
| Mon, 25 Apr 2016 16:09:26 +0200 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 16:52:56 +0100 |
paulson |
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
|
file |
diff |
annotate
|
| Sun, 03 Apr 2016 23:03:30 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Wed, 16 Mar 2016 13:57:06 +0000 |
paulson |
Contractible sets. Also removal of obsolete theorems and refactoring
|
file |
diff |
annotate
|
| Tue, 15 Mar 2016 14:08:25 +0000 |
paulson |
rationalisation of theorem names esp about "real Archimedian" etc.
|
file |
diff |
annotate
|
| Mon, 14 Mar 2016 15:58:02 +0000 |
paulson |
New results about paths, segments, etc. The notion of simply_connected.
|
file |
diff |
annotate
|
| Mon, 14 Mar 2016 14:19:06 +0000 |
paulson |
Refactoring (moving theorems into better locations), plus a bit of new material
|
file |
diff |
annotate
|
| Wed, 09 Mar 2016 17:16:08 +0000 |
paulson |
Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
|
file |
diff |
annotate
|
| Mon, 07 Mar 2016 15:57:02 +0000 |
paulson |
complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
|
file |
diff |
annotate
|
| Mon, 07 Mar 2016 14:34:45 +0000 |
paulson |
new material to Blochj's theorem, as well as supporting lemmas
|
file |
diff |
annotate
|
| Mon, 29 Feb 2016 15:13:11 +0000 |
paulson |
Merge
|
file |
diff |
annotate
|
| Mon, 29 Feb 2016 11:42:15 +0000 |
paulson |
the integral is 0 when otherwise it would be undefined (also for contour integrals)
|
file |
diff |
annotate
|
| Sun, 28 Feb 2016 19:56:57 +0100 |
wenzelm |
proper document source;
|
file |
diff |
annotate
|
| Thu, 25 Feb 2016 13:58:48 +0000 |
paulson |
Conformal_mappings: a big development in complex analysis (+ some lemmas)
|
file |
diff |
annotate
|
| Wed, 24 Feb 2016 16:00:57 +0000 |
paulson |
Merge
|
file |
diff |
annotate
|
| Wed, 24 Feb 2016 15:51:01 +0000 |
paulson |
Substantial new material for multivariate analysis. Also removal of some duplicates.
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Mon, 22 Feb 2016 14:37:56 +0000 |
paulson |
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:56 +0100 |
haftmann |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
file |
diff |
annotate
|
| Fri, 22 Jan 2016 16:00:03 +0000 |
paulson |
Reorganised a huge proof
|
file |
diff |
annotate
|
| Wed, 13 Jan 2016 23:07:06 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Mon, 11 Jan 2016 22:14:15 +0000 |
paulson |
nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
|
file |
diff |
annotate
|
| Fri, 08 Jan 2016 17:40:59 +0100 |
hoelzl |
add uniform spaces
|
file |
diff |
annotate
|
| Thu, 07 Jan 2016 17:40:55 +0000 |
paulson |
revisions to limits and derivatives, plus new lemmas
|
file |
diff |
annotate
|
| Wed, 30 Dec 2015 14:05:51 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Wed, 30 Dec 2015 11:37:29 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Wed, 30 Dec 2015 11:21:54 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 01:28:28 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Sun, 27 Dec 2015 21:46:36 +0100 |
wenzelm |
prefer symbols for "floor", "ceiling";
|
file |
diff |
annotate
|
| Tue, 22 Dec 2015 14:33:34 +0000 |
paulson |
Liouville theorem, Fundamental Theorem of Algebra, etc.
|
file |
diff |
annotate
|
| Tue, 15 Dec 2015 14:40:36 +0000 |
paulson |
New complex analysis material
|
file |
diff |
annotate
|
| Wed, 09 Dec 2015 17:35:22 +0000 |
paulson |
sorted out eventually_mono
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 20:19:59 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 16:44:26 +0000 |
paulson |
Cauchy's integral formula for circles. Starting to fix eventually_mono.
|
file |
diff |
annotate
|
| 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.
|
file |
diff |
annotate
|
| Mon, 23 Nov 2015 16:57:54 +0000 |
paulson |
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
|
file |
diff |
annotate
|
| Fri, 20 Nov 2015 14:44:53 +0000 |
paulson |
Theory of homotopic paths (from HOL Light), plus comments and minor refinements
|
file |
diff |
annotate
|
| Tue, 17 Nov 2015 12:32:08 +0000 |
paulson |
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
|
file |
diff |
annotate
|
| 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.
|
file |
diff |
annotate
|
| Tue, 27 Oct 2015 15:17:02 +0000 |
paulson |
Cauchy's integral formula, required lemmas, and a bit of reorganisation
|
file |
diff |
annotate
|
| Mon, 26 Oct 2015 23:41:27 +0000 |
paulson |
new lemmas about topology, etc., for Cauchy integral formula
|
file |
diff |
annotate
|
| Tue, 13 Oct 2015 12:42:08 +0100 |
paulson |
new material on path_component_sets, inside, outside, etc. And more default simprules
|
file |
diff |
annotate
|
| Wed, 30 Sep 2015 16:36:42 +0100 |
paulson |
real_of_nat_Suc is now a simprule
|
file |
diff |
annotate
|
| Mon, 21 Sep 2015 21:46:14 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Mon, 21 Sep 2015 19:52:13 +0100 |
paulson |
new lemmas and movement of lemmas into place
|
file |
diff |
annotate
|
| Sat, 19 Sep 2015 22:32:13 +0200 |
wenzelm |
eliminated hard tabs;
|
file |
diff |
annotate
|
| Fri, 18 Sep 2015 16:27:37 +0100 |
paulson |
Massive revisions, as a valid path must now be continously differentiable (C!)
|
file |
diff |
annotate
|
| Thu, 03 Sep 2015 20:27:53 +0100 |
paulson |
new lemmas about vector_derivative, complex numbers, paths, etc.
|
file |
diff |
annotate
|
| Tue, 28 Jul 2015 16:16:13 +0100 |
paulson |
the Cauchy integral theorem and related material
|
file |
diff |
annotate
|