| Fri, 20 Sep 2024 19:51:08 +0200 |
wenzelm |
standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing;
|
file |
diff |
annotate
|
| Sat, 09 Sep 2023 19:26:08 +0100 |
paulson |
Loads of new material related to porting the Euler Polyhedron Formula from HOL Light
|
file |
diff |
annotate
|
| Thu, 27 Jul 2023 23:05:25 +0100 |
paulson |
Cosmetic polishing of proofs
|
file |
diff |
annotate
|
| Tue, 25 Jul 2023 18:52:25 +0100 |
paulson |
A few more cosmetic changes to proofs
|
file |
diff |
annotate
|
| Tue, 03 Jan 2023 17:02:41 +0000 |
paulson |
More tidying of proofs
|
file |
diff |
annotate
|
| Tue, 13 Sep 2022 18:56:39 +0100 |
paulson |
Tidied a few more proofs
|
file |
diff |
annotate
|
| Fri, 15 Oct 2021 12:42:51 +0100 |
paulson |
A few new lemmas plus some refinements
|
file |
diff |
annotate
|
| Thu, 08 Jul 2021 08:42:36 +0200 |
desharna |
added opaque_combs and renamed hide_lams to opaque_lifting
|
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
|
| Mon, 28 Sep 2020 18:34:15 +0100 |
paulson |
de-applying
|
file |
diff |
annotate
|
| Fri, 25 Sep 2020 14:11:48 +0100 |
paulson |
fixed some remarkably ugly proofs
|
file |
diff |
annotate
|
| Thu, 14 May 2020 13:44:44 +0200 |
Manuel Eberl |
Tuned some proofs in HOL-Analysis
|
file |
diff |
annotate
|
| Sun, 19 Apr 2020 22:16:57 +0100 |
paulson |
removal of symmetries in Polytope, plus some tidying
|
file |
diff |
annotate
|
| Tue, 31 Mar 2020 15:51:15 +0200 |
nipkow |
cleaned proofs
|
file |
diff |
annotate
|
| Fri, 06 Dec 2019 17:03:58 +0100 |
nipkow |
cleaning
|
file |
diff |
annotate
|
| Wed, 09 Oct 2019 14:51:54 +0000 |
haftmann |
dedicated fact collections for algebraic simplification rules potentially splitting goals
|
file |
diff |
annotate
|
| Wed, 04 Sep 2019 14:16:27 +0100 |
paulson |
Theory Derivative no longer depends on Path_Connected
|
file |
diff |
annotate
|
| Fri, 12 Apr 2019 22:09:25 +0200 |
wenzelm |
modernized tags: default scope excludes proof;
|
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
|
| Mon, 28 Jan 2019 10:27:47 +0100 |
nipkow |
more canonical and less specialized syntax
|
file |
diff |
annotate
|
| Thu, 24 Jan 2019 00:28:29 +0000 |
Angeliki KoutsoukouArgyraki |
tagged 5 theories
|
file |
diff |
annotate
|
| Thu, 17 Jan 2019 16:38:00 -0500 |
immler |
subsection is always %important
|
file |
diff |
annotate
|
| Mon, 14 Jan 2019 18:35:03 +0000 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Thu, 27 Dec 2018 19:48:28 +0100 |
nipkow |
tuned headers; ~ -> \<not>
|
file |
diff |
annotate
|
| Sun, 18 Nov 2018 18:07:51 +0000 |
haftmann |
removed legacy input syntax
|
file |
diff |
annotate
|
| Thu, 08 Nov 2018 09:11:52 +0100 |
haftmann |
removed relics of ASCII syntax for indexed big operators
|
file |
diff |
annotate
|
| Tue, 28 Aug 2018 13:28:39 +0100 |
Angeliki KoutsoukouArgyraki |
tagged 21 theories in the Analysis library for the manual
|
file |
diff |
annotate
|
| Thu, 03 May 2018 16:17:44 +0200 |
immler |
fixed HOL-Analysis
|
file |
diff |
annotate
|
| Thu, 03 May 2018 15:07:14 +0200 |
immler |
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
|
file |
diff |
annotate
|