| 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
|
| Tue, 30 May 2023 12:33:06 +0100 |
paulson |
New HOL Light material on metric spaces and topological spaces
|
file |
diff |
annotate
|
| Sun, 01 Jan 2023 00:45:55 +0000 |
paulson |
Big simplifications of old proofs
|
file |
diff |
annotate
|
| Tue, 17 May 2022 14:10:14 +0100 |
paulson |
tidied auto / simp with null arguments
|
file |
diff |
annotate
|
| Sun, 07 Nov 2021 22:14:40 +0000 |
paulson |
new lemmas about convex, concave functions, + tidying
|
file |
diff |
annotate
|
| Thu, 08 Jul 2021 08:44:18 +0200 |
desharna |
merged
|
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
|
| Mon, 28 Jun 2021 15:05:46 +0100 |
paulson |
A few useful lemmas about derivatives, colinearity and other topics
|
file |
diff |
annotate
|
| Thu, 03 Jun 2021 10:47:20 +0100 |
paulson |
new lemmas mostly about paths
|
file |
diff |
annotate
|
| Sun, 09 May 2021 05:48:50 +0000 |
haftmann |
more elementary swap
|
file |
diff |
annotate
|
| Thu, 14 Nov 2019 11:54:52 +0100 |
nipkow |
tuned tags
|
file |
diff |
annotate
|
| Tue, 05 Nov 2019 21:07:03 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Tue, 05 Nov 2019 19:55:42 +0100 |
nipkow |
moved duplicate lemmas up the hierarchy
|
file |
diff |
annotate
|
| Tue, 05 Nov 2019 19:13:47 +0100 |
nipkow |
removed redundant lemma
|
file |
diff |
annotate
|
| Sat, 02 Nov 2019 14:31:34 +0000 |
paulson |
Inverse function theorem + lemmas
|
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
|
| Mon, 16 Sep 2019 17:03:13 +0100 |
paulson |
A little-known material, and some tidying up
|
file |
diff |
annotate
|
| Thu, 12 Sep 2019 14:51:45 +0100 |
paulson |
new material on Analysis, plus some rearrangements
|
file |
diff |
annotate
|
| Fri, 12 Apr 2019 22:09:25 +0200 |
wenzelm |
modernized tags: default scope excludes proof;
|
file |
diff |
annotate
|
| Thu, 17 Jan 2019 16:38:00 -0500 |
immler |
subsection is always %important
|
file |
diff |
annotate
|
| Wed, 16 Jan 2019 18:14:02 -0500 |
immler |
Reorg, in particular Determinants as well as some linear algebra from Starlike and Change_Of_Vars
|
file |
diff |
annotate
|
| Wed, 16 Jan 2019 16:50:35 -0500 |
immler |
bundle syntax for inner
|
file |
diff |
annotate
|
| Mon, 07 Jan 2019 14:06:54 +0100 |
immler |
split off Convex.thy: material that does not require Topology_Euclidean_Space
|
file |
diff |
annotate
|
| Sun, 06 Jan 2019 12:32:01 +0100 |
nipkow |
typed definitions
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Fri, 28 Dec 2018 10:29:59 +0100 |
nipkow |
tuned style and headers
|
file |
diff |
annotate
|
| Thu, 27 Dec 2018 23:38:55 +0100 |
immler |
most of Topology_Euclidean_Space (now Elementary_Topology) requires fewer dependencies
|
file |
diff |
annotate
|
| Thu, 27 Dec 2018 21:32:36 +0100 |
immler |
moved lemmas up
|
file |
diff |
annotate
|
| Thu, 27 Dec 2018 21:00:50 +0100 |
immler |
generalized to big sum
|
file |
diff |
annotate
|
| Mon, 03 Sep 2018 22:38:23 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|