| Mon, 03 Jul 2023 11:45:59 +0100 |
paulson |
EXPERIMENTAL replacement of f ` A <= B by f : A -> B in Analysis
|
file |
diff |
annotate
|
| Thu, 01 Jun 2023 12:08:33 +0100 |
paulson |
Even more material from the HOL Light metric space library
|
file |
diff |
annotate
|
| Tue, 02 May 2023 15:17:39 +0100 |
paulson |
More new theorems, and a necessary correction
|
file |
diff |
annotate
|
| Tue, 28 Feb 2023 16:46:56 +0000 |
paulson |
Imported a theorem about Infinite_Sum. Importing this theory a bit earlier is causing syntactic ambiguities with Infinite_Set_Sum however; no_notation needed
|
file |
diff |
annotate
|
| Wed, 11 Jan 2023 17:02:52 +0000 |
paulson |
More tidying of topology proofs
|
file |
diff |
annotate
|
| Wed, 11 Jan 2023 13:41:53 +0000 |
paulson |
Partial round of clearing up applys, etc
|
file |
diff |
annotate
|
| Mon, 02 Jan 2023 20:46:24 +0000 |
paulson |
Tidying up of paths, introducing "loop_free" as a separate predicate in the definition of "simple_path"
|
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
|
| Tue, 08 Sep 2020 15:30:15 +0100 |
paulson |
tidying and de-applying
|
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:58:32 +0100 |
paulson |
Sketch and explore again
|
file |
diff |
annotate
|
| Sun, 19 Apr 2020 22:16:57 +0100 |
paulson |
removal of symmetries in Polytope, plus some tidying
|
file |
diff |
annotate
|
| Sun, 12 Apr 2020 10:51:51 +0100 |
paulson |
cleaning up Homotopy
|
file |
diff |
annotate
|
| Tue, 31 Mar 2020 15:51:15 +0200 |
nipkow |
cleaned proofs
|
file |
diff |
annotate
|
| Thu, 28 Nov 2019 23:06:22 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Sat, 02 Nov 2019 15:52:47 +0000 |
paulson |
reorganisation to eliminate Brouwer_Fixpoint from complex analysis
|
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 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
|
| Thu, 15 Aug 2019 16:11:56 +0100 |
paulson |
new material; rotated premises of Lim_transform_eventually
|
file |
diff |
annotate
|
| Fri, 26 Apr 2019 16:51:40 +0100 |
paulson |
Added embedding_map_into_euclideanreal; reduced dependence on Equivalence_Lebesgue_Henstock_Integration in Analysis theories by moving a few lemmas
|
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
|
| 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
|
| Tue, 22 Jan 2019 22:57:16 +0000 |
Angeliki KoutsoukouArgyraki |
minor tagging updates in 13 theories
|
file |
diff |
annotate
|
| Tue, 22 Jan 2019 12:00:16 +0000 |
paulson |
renamings and new material
|
file |
diff |
annotate
|
| Thu, 17 Jan 2019 16:38:00 -0500 |
immler |
subsection is always %important
|
file |
diff |
annotate
|
| Thu, 17 Jan 2019 16:28:07 -0500 |
immler |
redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
|
file |
diff |
annotate
|
| Thu, 17 Jan 2019 16:22:21 -0500 |
immler |
revert to 56acd449da41
|
file |
diff |
annotate
|