| Mon, 03 Jul 2023 11:45:59 +0100 |
paulson |
EXPERIMENTAL replacement of f ` A <= B by f : A -> B in Analysis
|
file |
diff |
annotate
|
| Mon, 15 May 2023 17:12:18 +0100 |
paulson |
More material from the HOL Light metric space library
|
file |
diff |
annotate
|
| Sun, 07 Nov 2021 22:14:40 +0000 |
paulson |
new lemmas about convex, concave functions, + tidying
|
file |
diff |
annotate
|
| Fri, 16 Jul 2021 14:43:25 +0100 |
paulson |
A few new lemmas and simplifications
|
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
|
| Tue, 10 Nov 2020 23:21:04 +0000 |
paulson |
cleanup
|
file |
diff |
annotate
|
| Fri, 25 Sep 2020 14:11:48 +0100 |
paulson |
fixed some remarkably ugly proofs
|
file |
diff |
annotate
|
| Fri, 04 Sep 2020 17:32:42 +0100 |
paulson |
a bit of tidying
|
file |
diff |
annotate
|
| Sun, 30 Aug 2020 19:45:46 +0100 |
paulson |
minor tidying, also s->S and t->T
|
file |
diff |
annotate
|
| Wed, 26 Aug 2020 15:59:21 +0100 |
paulson |
tiny tidy-up of proofs
|
file |
diff |
annotate
|
| Sat, 23 May 2020 21:24:33 +0100 |
paulson |
a few new lemmas about functions
|
file |
diff |
annotate
|
| Tue, 31 Mar 2020 15:51:15 +0200 |
nipkow |
cleaned proofs
|
file |
diff |
annotate
|
| Mon, 09 Dec 2019 15:36:51 +0000 |
paulson |
a few new and tidier proofs (mostly about finite sets)
|
file |
diff |
annotate
|
| Fri, 06 Dec 2019 17:03:58 +0100 |
nipkow |
cleaning
|
file |
diff |
annotate
|
| Thu, 05 Dec 2019 18:26:11 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Thu, 05 Dec 2019 11:21:17 +0100 |
nipkow |
made Starlike independent of Abstract_Limits
|
file |
diff |
annotate
|
| Wed, 04 Dec 2019 23:11:29 +0100 |
nipkow |
moved starlike where it belongs
|
file |
diff |
annotate
|
| Wed, 04 Dec 2019 18:28:24 +0100 |
nipkow |
moved segment lemmas where they belong
|
file |
diff |
annotate
|
| Wed, 04 Dec 2019 14:12:59 +0100 |
nipkow |
moved lemmas
|
file |
diff |
annotate
|
| Wed, 04 Dec 2019 12:00:07 +0100 |
nipkow |
moved lemma
|
file |
diff |
annotate
|
| Fri, 29 Nov 2019 21:29:18 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Fri, 29 Nov 2019 15:06:04 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Thu, 28 Nov 2019 23:06:22 +0100 |
nipkow |
tuned
|
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:26:20 -0500 |
immler |
betweenness is a property on line segments
|
file |
diff |
annotate
|
| Sat, 02 Nov 2019 21:42:45 +0000 |
paulson |
moved line segments to Convex_Euclidean_Space
|
file |
diff |
annotate
|
| Sat, 02 Nov 2019 20:51:54 +0000 |
paulson |
just tidied one proof
|
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
|