src/HOL/Analysis/Line_Segment.thy
Thu, 08 Jul 2021 08:42:36 +0200 desharna added opaque_combs and renamed hide_lams to opaque_lifting
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
Sun, 08 Dec 2019 17:42:53 +0100 nipkow moved lemmas
Wed, 04 Dec 2019 18:28:24 +0100 nipkow moved segment lemmas where they belong
Sat, 30 Nov 2019 13:47:33 +0100 Manuel Eberl Split off new HOL-Complex_Analysis session from HOL-Analysis
Thu, 28 Nov 2019 16:43:02 +0000 paulson Fixed a few messy proofs and adjusted inconsistent section headings
Mon, 04 Nov 2019 19:53:43 -0500 immler Line_Segment is independent of Convex_Euclidean_Space
less more (0) tip