| Fri, 04 Aug 2023 19:17:49 +0200 |
paulson |
Removal of ugly old proofs
|
file |
diff |
annotate
|
| Tue, 31 Jan 2023 14:05:16 +0000 |
paulson |
Lots more new material thanks to Manuel Eberl
|
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
|
| Sun, 08 Dec 2019 17:42:53 +0100 |
nipkow |
moved lemmas
|
file |
diff |
annotate
|
| Wed, 04 Dec 2019 18:28:24 +0100 |
nipkow |
moved segment lemmas where they belong
|
file |
diff |
annotate
|
| Sat, 30 Nov 2019 13:47:33 +0100 |
Manuel Eberl |
Split off new HOL-Complex_Analysis session from HOL-Analysis
|
file |
diff |
annotate
|
| Thu, 28 Nov 2019 16:43:02 +0000 |
paulson |
Fixed a few messy proofs and adjusted inconsistent section headings
|
file |
diff |
annotate
|
| Mon, 04 Nov 2019 19:53:43 -0500 |
immler |
Line_Segment is independent of Convex_Euclidean_Space
|
file |
diff |
annotate
|