| Thu, 27 Jul 2023 23:05:25 +0100 |
paulson |
Cosmetic polishing of proofs
|
file |
diff |
annotate
|
| Mon, 17 Jul 2023 21:49:49 +0100 |
paulson |
tidying a few proofs a bit more
|
file |
diff |
annotate
|
| Sat, 15 Jul 2023 23:34:42 +0100 |
paulson |
trivial_topology
|
file |
diff |
annotate
|
| Mon, 03 Jul 2023 11:45:59 +0100 |
paulson |
EXPERIMENTAL replacement of f ` A <= B by f : A -> B in Analysis
|
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
|
| Fri, 17 Mar 2023 17:06:28 +0000 |
paulson |
Numerous significant simplifications
|
file |
diff |
annotate
|
| Fri, 17 Mar 2023 10:42:39 +0000 |
paulson |
Proof simplification
|
file |
diff |
annotate
|
| Mon, 06 Feb 2023 15:41:23 +0000 |
paulson |
Some more new material and some tidying of existing proofs
|
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
|
| Sat, 03 Oct 2020 20:47:37 +0100 |
paulson |
de-applying
|
file |
diff |
annotate
|
| Sun, 19 Apr 2020 13:01:40 +0100 |
paulson |
Sketch_and_Explore — oops
|
file |
diff |
annotate
|
| Sun, 19 Apr 2020 12:02:26 +0100 |
paulson |
the rest of the applys
|
file |
diff |
annotate
|
| Sat, 18 Apr 2020 23:13:17 +0100 |
paulson |
more applys
|
file |
diff |
annotate
|
| Sun, 12 Apr 2020 21:53:58 +0100 |
paulson |
more cleaning up Homotopy
|
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
|
| Wed, 04 Dec 2019 23:11:29 +0100 |
nipkow |
moved starlike where it belongs
|
file |
diff |
annotate
|
| Thu, 28 Nov 2019 23:06:22 +0100 |
nipkow |
tuned
|
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
|
| Tue, 08 Oct 2019 10:26:40 +0000 |
haftmann |
formally augmented corresponding rules for field_simps
|
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, 02 Apr 2019 14:51:27 +0200 |
wenzelm |
eliminated hard TABs;
|
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, 18 Mar 2019 15:35:34 +0000 |
paulson |
new material;' strengthened material; moved proofs out of Function_Topology in order to lessen its dependencies
|
file |
diff |
annotate
|
| Thu, 31 Jan 2019 13:08:59 +0000 |
haftmann |
proper congruence rule for image operator
|
file |
diff |
annotate
|
| Tue, 22 Jan 2019 12:00:16 +0000 |
paulson |
renamings and new material
|
file |
diff |
annotate
|
| Mon, 07 Jan 2019 14:57:45 +0100 |
immler |
split off Homotopy.thy
|
file |
diff |
annotate
|