| 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
|