| Mon, 11 Apr 2016 16:27:42 +0100 |
paulson |
lots of new theorems for multivariate analysis
|
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
|
| Wed, 16 Mar 2016 13:57:06 +0000 |
paulson |
Contractible sets. Also removal of obsolete theorems and refactoring
|
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
|
| Mon, 07 Mar 2016 14:34:45 +0000 |
paulson |
new material to Blochj's theorem, as well as supporting 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 18:04:31 +0100 |
nipkow |
resolved conflict
|
file |
diff |
annotate
|
| 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
|
| Mon, 11 Jan 2016 22:14:15 +0000 |
paulson |
nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
|
file |
diff |
annotate
|
| Fri, 08 Jan 2016 15:49:01 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 07 Jan 2016 13:42:43 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 07 Jan 2016 17:40:55 +0000 |
paulson |
revisions to limits and derivatives, plus new lemmas
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 17:43:30 +0100 |
wenzelm |
prefer symbols for "Union", "Inter";
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 01:28:28 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Thu, 17 Dec 2015 16:43:36 +0100 |
hoelzl |
moved some theorems from the CLT proof; reordered some theorems / notation
|
file |
diff |
annotate
|
| Tue, 15 Dec 2015 14:40:36 +0000 |
paulson |
New complex analysis material
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 20:19:59 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
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
|
| 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
|
| Mon, 02 Nov 2015 11:56:28 +0100 |
eberlm |
Rounding function, uniform limits, cotangent, binomial identities
|
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
|
| Mon, 21 Sep 2015 21:46:14 +0200 |
wenzelm |
isabelle update_cartouches;
|
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, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
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
|
| Mon, 27 Jul 2015 16:52:57 +0100 |
paulson |
New material for Cauchy's integral theorem
|
file |
diff |
annotate
|
| Mon, 20 Jul 2015 23:12:50 +0100 |
paulson |
new material for multivariate analysis, etc.
|
file |
diff |
annotate
|
| Fri, 26 Jun 2015 10:20:33 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Wed, 10 Jun 2015 19:10:20 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Thu, 28 May 2015 14:33:35 +0100 |
paulson |
Convex hulls: theorems about interior, etc. And a few simple lemmas.
|
file |
diff |
annotate
|
| Tue, 26 May 2015 21:58:04 +0100 |
paulson |
New material about paths, and some lemmas
|
file |
diff |
annotate
|
| Tue, 05 May 2015 18:45:10 +0200 |
immler |
closures of intervals
|
file |
diff |
annotate
|
| Wed, 25 Mar 2015 10:44:57 +0100 |
wenzelm |
prefer local fixes;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:09:04 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Fri, 24 Oct 2014 15:07:51 +0200 |
hoelzl |
use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
|
file |
diff |
annotate
|
| Tue, 05 Aug 2014 16:58:19 +0200 |
wenzelm |
tuned proofs -- fewer warnings;
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
| Mon, 30 Jun 2014 15:45:21 +0200 |
hoelzl |
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
|
file |
diff |
annotate
|
| Sat, 28 Jun 2014 09:16:42 +0200 |
haftmann |
fact consolidation
|
file |
diff |
annotate
|
| Wed, 07 May 2014 12:25:35 +0200 |
hoelzl |
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
|
file |
diff |
annotate
|
| Mon, 14 Apr 2014 13:08:17 +0200 |
hoelzl |
added divide_nonneg_nonneg and co; made it a simp rule
|
file |
diff |
annotate
|
| Sat, 12 Apr 2014 17:26:27 +0200 |
nipkow |
made mult_pos_pos a simp rule
|
file |
diff |
annotate
|
| Fri, 11 Apr 2014 22:53:33 +0200 |
nipkow |
made divide_pos_pos a simp rule
|
file |
diff |
annotate
|
| Fri, 11 Apr 2014 13:36:57 +0200 |
nipkow |
made mult_nonneg_nonneg a simp rule
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 09:37:48 +0200 |
hoelzl |
field_simps: better support for negation and division, and power
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 09:37:47 +0200 |
hoelzl |
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
|
file |
diff |
annotate
|
| Thu, 03 Apr 2014 23:51:52 +0100 |
paulson |
removing simprule status for divide_minus_left and divide_minus_right
|
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
|
| Wed, 02 Apr 2014 18:35:01 +0200 |
hoelzl |
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 09:39:07 -0700 |
huffman |
remove unnecessary finiteness assumptions from lemmas about setsum
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 10:12:58 +0100 |
immler |
removed dependencies on theory Ordered_Euclidean_Space
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 10:12:57 +0100 |
immler |
use cbox to relax class constraints
|
file |
diff |
annotate
|