| Fri, 18 Oct 2024 14:37:09 +0200 |
wenzelm |
clarified syntax declarations: keep things together;
|
file |
diff |
annotate
|
| Fri, 20 Sep 2024 19:51:08 +0200 |
wenzelm |
standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing;
|
file |
diff |
annotate
|
| Mon, 06 May 2024 14:39:33 +0100 |
paulson |
Some new simprules – and patches for proofs
|
file |
diff |
annotate
|
| Wed, 14 Feb 2024 15:33:45 +0000 |
paulson |
the syntax of Lebesgue integrals (LINT, LBINT, ∫, etc.) now requires parentheses
|
file |
diff |
annotate
|
| Fri, 02 Feb 2024 11:25:11 +0000 |
paulson |
A small number of new lemmas
|
file |
diff |
annotate
|
| Sat, 12 Aug 2023 10:09:29 +0100 |
paulson |
substantial tidy-up, shortening many proofs
|
file |
diff |
annotate
|
| Mon, 20 Feb 2023 15:19:53 +0000 |
paulson |
Replacing z powr of_int i by z powi i and adding new material from the AFP
|
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, 27 Jan 2022 12:25:24 +0000 |
paulson |
useful lemma integral_less
|
file |
diff |
annotate
|
| Sun, 09 Jan 2022 18:50:06 +0000 |
paulson |
Some lemmas about continuous functions with integral zero
|
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, 07 Apr 2021 12:28:19 +0000 |
haftmann |
simplified definition
|
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
|
| Thu, 29 Oct 2020 23:26:44 +0000 |
paulson |
a further clean up
|
file |
diff |
annotate
|
| Tue, 31 Mar 2020 15:51:15 +0200 |
nipkow |
cleaned proofs
|
file |
diff |
annotate
|
| Fri, 06 Dec 2019 17:03:58 +0100 |
nipkow |
cleaning
|
file |
diff |
annotate
|
| Mon, 02 Dec 2019 14:22:03 +0100 |
Manuel Eberl |
Flattened dependency tree of HOL-Analysis
|
file |
diff |
annotate
|
| Fri, 29 Nov 2019 15:06:04 +0100 |
nipkow |
tuned
|
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
|
| Thu, 19 Sep 2019 14:49:19 +0100 |
paulson |
one small last theorem
|
file |
diff |
annotate
|
| Tue, 17 Sep 2019 12:36:04 +0100 |
paulson |
A few new theorems, tidying up and deletion of obsolete material
|
file |
diff |
annotate
|
| Mon, 16 Sep 2019 17:03:13 +0100 |
paulson |
A little-known material, and some tidying up
|
file |
diff |
annotate
|
| Fri, 13 Sep 2019 12:46:36 +0100 |
paulson |
New theory Equivalence_Measurable_On_Borel, with the HOL Light notion of measurable_on and its equivalence to ours
|
file |
diff |
annotate
|
| Thu, 12 Sep 2019 14:51:45 +0100 |
paulson |
new material on Analysis, plus some rearrangements
|
file |
diff |
annotate
|
| Wed, 28 Aug 2019 00:08:14 +0200 |
immler |
removed Brouwer_Fixpoint from imports of Derivative
|
file |
diff |
annotate
|
| Fri, 16 Aug 2019 12:53:36 +0100 |
paulson |
new material on eqiintegrable functions, etc.
|
file |
diff |
annotate
|
| Thu, 15 Aug 2019 16:11:56 +0100 |
paulson |
new material; rotated premises of Lim_transform_eventually
|
file |
diff |
annotate
|
| Fri, 19 Jul 2019 12:57:14 +0100 |
paulson |
More results about measure and integration theory
|
file |
diff |
annotate
|
| Thu, 18 Jul 2019 15:40:15 +0100 |
paulson |
More analysis / measure theory material
|
file |
diff |
annotate
|
| Thu, 18 Jul 2019 14:08:28 +0100 |
paulson |
more new material about analysis
|
file |
diff |
annotate
|
| Wed, 17 Jul 2019 14:02:42 +0100 |
paulson |
a few new lemmas and a bit of tidying
|
file |
diff |
annotate
|
| Wed, 15 May 2019 14:43:32 +0100 |
paulson |
a few general lemmas
|
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, 14 Jan 2019 18:35:03 +0000 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Thu, 27 Dec 2018 19:48:28 +0100 |
nipkow |
tuned headers; ~ -> \<not>
|
file |
diff |
annotate
|
| Thu, 22 Nov 2018 10:06:31 +0000 |
haftmann |
removed legacy input syntax
|
file |
diff |
annotate
|
| Sun, 18 Nov 2018 18:07:51 +0000 |
haftmann |
removed legacy input syntax
|
file |
diff |
annotate
|
| Sun, 11 Nov 2018 16:08:59 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Thu, 08 Nov 2018 09:11:52 +0100 |
haftmann |
removed relics of ASCII syntax for indexed big operators
|
file |
diff |
annotate
|
| Sat, 04 Aug 2018 01:03:39 +0200 |
eberlm |
Small lemmas about analysis
|
file |
diff |
annotate
|
| Thu, 28 Jun 2018 14:13:57 +0100 |
paulson |
Generalising and renaming some basic results
|
file |
diff |
annotate
|
| Wed, 06 Jun 2018 18:19:55 +0200 |
nipkow |
reorient -> split; documented split
|
file |
diff |
annotate
|
| Tue, 08 May 2018 10:32:07 +0100 |
paulson |
tidying more messy proofs
|
file |
diff |
annotate
|
| Thu, 03 May 2018 15:07:14 +0200 |
immler |
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
|
file |
diff |
annotate
|
| Wed, 02 May 2018 13:49:38 +0200 |
immler |
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
|
file |
diff |
annotate
|
| Thu, 26 Apr 2018 19:51:32 +0200 |
nipkow |
new simp modifier: reorient
|
file |
diff |
annotate
|
| Fri, 20 Apr 2018 19:11:17 +0100 |
paulson |
three new theorems
|
file |
diff |
annotate
|
| Tue, 17 Apr 2018 22:35:48 +0100 |
paulson |
Change of variables proof
|
file |
diff |
annotate
|
| Tue, 17 Apr 2018 10:22:42 +0100 |
paulson |
more about measure
|
file |
diff |
annotate
|
| Mon, 16 Apr 2018 21:23:38 +0100 |
paulson |
some more random results
|
file |
diff |
annotate
|
| Mon, 16 Apr 2018 15:00:46 +0100 |
paulson |
more results about measure and negligibility
|
file |
diff |
annotate
|
| Sun, 15 Apr 2018 21:41:40 +0100 |
paulson |
quite a few more results about negligibility, etc., and a bit of tidying up
|
file |
diff |
annotate
|
| Sun, 15 Apr 2018 17:22:47 +0100 |
paulson |
a few more results
|
file |
diff |
annotate
|
| Sun, 15 Apr 2018 13:57:00 +0100 |
paulson |
various new results on measures, integrals, etc., and some simplified proofs
|
file |
diff |
annotate
|
| Sat, 14 Apr 2018 20:19:52 +0100 |
paulson |
more new theorems on real^1, matrices, etc.
|
file |
diff |
annotate
|
| Sat, 14 Apr 2018 15:36:49 +0100 |
paulson |
a few new theorems and some fixes
|
file |
diff |
annotate
|