| Wed, 27 Mar 2024 15:16:09 +0000 |
paulson |
New material and a bit of refactoring
|
file |
diff |
annotate
|
| Thu, 02 Mar 2023 17:17:18 +0000 |
paulson |
Some new lemmas. Some tidying up
|
file |
diff |
annotate
|
| Sun, 01 Jan 2023 00:45:55 +0000 |
paulson |
Big simplifications of old proofs
|
file |
diff |
annotate
|
| Fri, 30 Dec 2022 23:21:37 +0000 |
paulson |
Continued proof simplifications
|
file |
diff |
annotate
|
| Tue, 24 May 2022 16:21:49 +0100 |
paulson |
Renamed the misleading has_field_derivative_iff_has_vector_derivative. Inserted a number of minor lemmas
|
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
|
| Sun, 08 Dec 2019 17:42:53 +0100 |
nipkow |
moved lemmas
|
file |
diff |
annotate
|
| Thu, 28 Nov 2019 23:06:22 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Tue, 05 Nov 2019 14:57:41 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Tue, 05 Nov 2019 12:00:23 +0000 |
paulson |
Merge and get rid of closed_segmentI
|
file |
diff |
annotate
|
| Mon, 04 Nov 2019 17:06:18 +0000 |
paulson |
Moved or deleted some out of place material, also eliminating obsolete naming conventions
|
file |
diff |
annotate
|
| Mon, 04 Nov 2019 19:53:43 -0500 |
immler |
Line_Segment is independent of Convex_Euclidean_Space
|
file |
diff |
annotate
|
| Mon, 04 Nov 2019 17:18:25 -0500 |
immler |
reduce dependencies of Ordered_Euclidean_Space; move more general material from Cartesian_Euclidean_Space
|
file |
diff |
annotate
|
| Sun, 27 Oct 2019 17:26:50 +0100 |
immler |
example applications of the 'metric' decision procedure, by Maximilian Schäffeler
|
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, 12 Apr 2019 22:09:25 +0200 |
wenzelm |
modernized tags: default scope excludes proof;
|
file |
diff |
annotate
|
| Mon, 08 Apr 2019 15:26:54 +0100 |
paulson |
First tranche of the Homology development: Simplices
|
file |
diff |
annotate
|
| Fri, 05 Apr 2019 15:02:46 +0100 |
paulson |
Free_Abelian_Groups finally working; fixed some duplicates; cleaned up some proofs
|
file |
diff |
annotate
|
| Mon, 01 Apr 2019 17:02:43 +0100 |
paulson |
A few results in Algebra, and bits for Analysis
|
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
|
| Tue, 29 Jan 2019 16:13:11 +0100 |
nipkow |
moved generalized material
|
file |
diff |
annotate
|
| Fri, 25 Jan 2019 14:19:19 -0500 |
immler |
generalized
|
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
|
| Wed, 16 Jan 2019 19:34:48 -0500 |
immler |
chapters for analysis manual
|
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
|
| Mon, 07 Jan 2019 13:33:29 +0100 |
immler |
moved setdist to more appropriate places
|
file |
diff |
annotate
|
| Mon, 07 Jan 2019 13:16:33 +0100 |
immler |
reduced dependencies of Connected.thy
|
file |
diff |
annotate
|