| Sun, 09 May 2021 05:48:50 +0000 |
haftmann |
more elementary swap
|
file |
diff |
annotate
|
| Mon, 22 Mar 2021 10:49:51 +0000 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| Wed, 11 Nov 2020 14:27:17 +0000 |
paulson |
mult_le_cancel_iff1, mult_le_cancel_iff2, mult_less_iff1 generalised from the real_ versions
|
file |
diff |
annotate
|
| Fri, 25 Sep 2020 14:11:48 +0100 |
paulson |
fixed some remarkably ugly proofs
|
file |
diff |
annotate
|
| Sun, 12 Apr 2020 10:51:51 +0100 |
paulson |
cleaning up Homotopy
|
file |
diff |
annotate
|
| Sun, 16 Feb 2020 18:01:03 +0100 |
nipkow |
lemmas about "card A = 2"; prefer iff to implications
|
file |
diff |
annotate
|
| Thu, 28 Nov 2019 23:06:22 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Tue, 08 Oct 2019 10:26:40 +0000 |
haftmann |
formally augmented corresponding rules for field_simps
|
file |
diff |
annotate
|
| Wed, 04 Sep 2019 16:34:45 +0100 |
paulson |
Removal of the redundant ancestor Continuous_Extension
|
file |
diff |
annotate
|
| Wed, 04 Sep 2019 15:27:04 +0100 |
paulson |
Half of Brouwer_Fixpoint split off to form a separate theory: Retracts.
|
file |
diff |
annotate
|
| Wed, 28 Aug 2019 00:08:14 +0200 |
immler |
removed Brouwer_Fixpoint from imports of Derivative
|
file |
diff |
annotate
|
| Fri, 12 Apr 2019 22:09:25 +0200 |
wenzelm |
modernized tags: default scope excludes proof;
|
file |
diff |
annotate
|
| Tue, 26 Mar 2019 17:01:36 +0000 |
paulson |
generalised homotopic_with to topologies; homotopic_with_canon is the old version
|
file |
diff |
annotate
|
| Fri, 22 Mar 2019 12:34:49 +0000 |
paulson |
New abstract topological material
|
file |
diff |
annotate
|
| Tue, 19 Mar 2019 16:14:51 +0000 |
paulson |
new material about topology, etc.; also fixes for yesterday's
|
file |
diff |
annotate
|
| Fri, 25 Jan 2019 13:19:16 +0100 |
nipkow |
moved retracts
|
file |
diff |
annotate
|
| Tue, 22 Jan 2019 12:00:16 +0000 |
paulson |
renamings and new material
|
file |
diff |
annotate
|
| Mon, 21 Jan 2019 14:44:23 +0000 |
paulson |
new material about summations and powers, along with some tweaks
|
file |
diff |
annotate
|
| Mon, 14 Jan 2019 18:35:03 +0000 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Mon, 07 Jan 2019 14:57:45 +0100 |
immler |
split off Homotopy.thy
|
file |
diff |
annotate
|
| Tue, 01 Jan 2019 21:47:27 +0100 |
wenzelm |
more antiquotations -- less LaTeX macros;
|
file |
diff |
annotate
|
| Sat, 29 Dec 2018 15:43:53 +0100 |
nipkow |
capitalize proper names in lemma names
|
file |
diff |
annotate
|
| Thu, 27 Dec 2018 19:48:28 +0100 |
nipkow |
tuned headers; ~ -> \<not>
|
file |
diff |
annotate
|
| Thu, 22 Nov 2018 10:06:31 +0000 |
haftmann |
removed legacy input syntax
|
file |
diff |
annotate
|
| Sun, 18 Nov 2018 18:07:51 +0000 |
haftmann |
removed legacy input syntax
|
file |
diff |
annotate
|
| Sun, 11 Nov 2018 16:08:59 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Fri, 13 Jul 2018 12:40:35 +0200 |
nipkow |
unit_cube = cbox 0 One
|
file |
diff |
annotate
|
| Thu, 12 Jul 2018 11:23:46 +0200 |
nipkow |
more economic tagging
|
file |
diff |
annotate
|
| Sun, 03 Jun 2018 15:22:30 +0100 |
paulson |
infinite product material
|
file |
diff |
annotate
|
| Sat, 26 May 2018 22:11:55 +0100 |
paulson |
tidying and reorganisation around Cauchy Integral Theorem
|
file |
diff |
annotate
|