| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 15:47:39 +0000 |
paulson |
New and revised material for (multivariate) analysis
|
file |
diff |
annotate
|
| Thu, 07 Jan 2016 17:40:55 +0000 |
paulson |
revisions to limits and derivatives, plus new lemmas
|
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
|
| Wed, 18 Nov 2015 15:23:34 +0000 |
paulson |
New theorems mostly from Peter Gammie
|
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
|
| 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
|
| Mon, 21 Sep 2015 19:52:13 +0100 |
paulson |
new lemmas and movement of lemmas into place
|
file |
diff |
annotate
|
| Wed, 19 Aug 2015 19:18:19 +0100 |
paulson |
New material and fixes related to the forthcoming Stone-Weierstrass development
|
file |
diff |
annotate
|
| Tue, 28 Jul 2015 16:16:13 +0100 |
paulson |
the Cauchy integral theorem and related material
|
file |
diff |
annotate
|
| Wed, 10 Jun 2015 19:10:20 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Tue, 26 May 2015 21:58:04 +0100 |
paulson |
New material about paths, and some lemmas
|
file |
diff |
annotate
|
| Thu, 19 Feb 2015 11:53:36 +0100 |
haftmann |
establish unique preferred fact names
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:09:04 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Wed, 02 Apr 2014 18:35:07 +0200 |
hoelzl |
extend continuous_intros; remove continuous_on_intros and isCont_intros
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 10:12:57 +0100 |
immler |
use cbox to relax class constraints
|
file |
diff |
annotate
|
| Sat, 14 Sep 2013 23:52:36 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Thu, 12 Sep 2013 09:03:52 -0700 |
huffman |
removed outdated comments
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
|
file |
diff |
annotate
|
| 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)
|
file |
diff |
annotate
|
| Thu, 17 Jan 2013 11:57:17 +0100 |
hoelzl |
generalize compact_path_image to topological_space
|
file |
diff |
annotate
|
| Mon, 14 Jan 2013 18:30:36 +0100 |
hoelzl |
differentiate (cover) compactness and sequential compactness
|
file |
diff |
annotate
|
| Fri, 14 Dec 2012 15:46:01 +0100 |
hoelzl |
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
|
file |
diff |
annotate
|
| Fri, 28 Sep 2012 23:45:15 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 28 Sep 2012 23:40:48 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|