| Fri, 15 Jul 2016 12:17:16 +0200 |
hoelzl |
HOL-Multivariate_Analysis: add amssymb to document generation; reintroduce \nexists (cf d51a0a772094)
|
file |
diff |
annotate
|
| Thu, 14 Jul 2016 16:49:22 +0100 |
paulson |
Got rid of the \nexists macro
|
file |
diff |
annotate
|
| Thu, 14 Jul 2016 14:48:49 +0100 |
paulson |
More advanced theorems about retracts, homotopies., etc
|
file |
diff |
annotate
|
| Wed, 13 Jul 2016 17:14:17 +0100 |
paulson |
lots of new theorems about differentiable_on, retracts, ANRs, etc.
|
file |
diff |
annotate
|
| Sat, 02 Jul 2016 08:41:05 +0200 |
haftmann |
more theorems
|
file |
diff |
annotate
|
| Wed, 15 Jun 2016 22:19:03 +0200 |
hoelzl |
move open_Collect_eq/less to HOL
|
file |
diff |
annotate
|
| Thu, 16 Jun 2016 12:05:04 +0100 |
paulson |
Removed instances of ^ from theory markup
|
file |
diff |
annotate
|
| Wed, 15 Jun 2016 15:52:24 +0100 |
paulson |
Urysohn's lemma, Dugundji extension theorem and many other proofs
|
file |
diff |
annotate
|
| Tue, 14 Jun 2016 15:34:21 +0100 |
paulson |
new results about topology
|
file |
diff |
annotate
|
| Tue, 24 May 2016 15:08:07 +0100 |
paulson |
Merge
|
file |
diff |
annotate
|
| Mon, 25 Apr 2016 16:09:26 +0200 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
| 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
|
| 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
|
| Tue, 05 Jan 2016 15:35:08 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 01:28:28 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 20:19:59 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
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
|
| Wed, 30 Sep 2015 16:36:42 +0100 |
paulson |
real_of_nat_Suc is now a simprule
|
file |
diff |
annotate
|
| Sun, 13 Sep 2015 22:56:52 +0200 |
wenzelm |
tuned proofs -- less legacy;
|
file |
diff |
annotate
|
| Thu, 25 Jun 2015 23:33:47 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 13 Jun 2015 13:09:05 +0200 |
wenzelm |
renamed "prems" to "that";
|
file |
diff |
annotate
|
| Wed, 10 Jun 2015 20:15:58 +0200 |
wenzelm |
misc tuning;
|
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
|
| Fri, 20 Mar 2015 16:11:28 +0000 |
paulson |
tweaked a few slow or very ugly proofs
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:09:04 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Sat, 28 Jun 2014 09:16:42 +0200 |
haftmann |
fact consolidation
|
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 11:27:36 +0200 |
haftmann |
more operations and lemmas
|
file |
diff |
annotate
|
| Fri, 11 Apr 2014 22:53:33 +0200 |
nipkow |
made divide_pos_pos a simp rule
|
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, 25 Mar 2014 14:20:58 +0100 |
hoelzl |
cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
|
file |
diff |
annotate
|
| Thu, 20 Mar 2014 09:21:39 -0700 |
huffman |
generalize some theorems
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 10:12:57 +0100 |
immler |
use cbox to relax class constraints
|
file |
diff |
annotate
|
| Sat, 15 Mar 2014 08:31:33 +0100 |
haftmann |
more complete set of lemmas wrt. image and composition
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 16:07:27 -0700 |
huffman |
remove ordered_euclidean_space constraint from brouwer/derivative lemmas;
|
file |
diff |
annotate
|
| Sun, 16 Feb 2014 21:09:47 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 16:11:14 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
prefer box over greaterThanLessThan on euclidean_space
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 17:37:45 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Wed, 18 Sep 2013 00:11:15 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 17 Sep 2013 00:13:20 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Wed, 28 Aug 2013 22:50:23 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Wed, 28 Aug 2013 17:20:16 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 24 Aug 2013 23:16:37 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 24 Aug 2013 21:23:40 +0200 |
wenzelm |
tuned proofs;
|
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
|
| 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
|
| Wed, 12 Dec 2012 22:37:06 +0100 |
blanchet |
tuned two lemma names, to avoid name hint clash (which confuses the MaSh evaluation, and which anyway isn't nice or necessary)
|
file |
diff |
annotate
|
| Thu, 08 Nov 2012 11:59:48 +0100 |
bulwahn |
adjusting proofs as the set_comprehension_pointfree simproc breaks some existing proofs
|
file |
diff |
annotate
|
| Mon, 24 Sep 2012 17:52:44 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 14 Sep 2012 21:26:01 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 09:02:58 -0700 |
huffman |
avoid using legacy theorem names
|
file |
diff |
annotate
|
| Tue, 23 Aug 2011 14:11:02 -0700 |
huffman |
declare euclidean_simps [simp] at the point they are proved;
|
file |
diff |
annotate
|