| 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
|
| Sat, 14 Apr 2018 09:23:00 +0100 |
paulson |
new material about vec, real^1, etc.
|
file |
diff |
annotate
|
| Wed, 11 Apr 2018 16:34:44 +0100 |
paulson |
replacement of set integral abbreviations by actual definitions!
|
file |
diff |
annotate
|
| Mon, 09 Apr 2018 17:20:58 +0100 |
paulson |
A couple of new results
|
file |
diff |
annotate
|
| Thu, 15 Feb 2018 12:11:00 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Thu, 31 Aug 2017 18:30:18 +0100 |
paulson |
more proof simplificaition
|
file |
diff |
annotate
|
| Tue, 29 Aug 2017 17:41:11 +0100 |
paulson |
last-minute integration unscrambling
|
file |
diff |
annotate
|
| Sat, 26 Aug 2017 00:43:26 +0100 |
paulson |
unscrambling esp of Henstock_lemma_part1
|
file |
diff |
annotate
|
| Fri, 25 Aug 2017 23:30:36 +0100 |
paulson |
starting to unscramble bounded_variation_absolutely_integrable_interval
|
file |
diff |
annotate
|
| Wed, 23 Aug 2017 23:46:35 +0100 |
paulson |
More tidying, and renaming of theorems
|
file |
diff |
annotate
|
| Tue, 15 Aug 2017 22:22:15 +0100 |
paulson |
fixed the previous commit (henstock_lemma)
|
file |
diff |
annotate
|
| Sun, 13 Aug 2017 19:24:33 +0100 |
paulson |
general rationalisation of Analysis
|
file |
diff |
annotate
|
| Sat, 05 Aug 2017 22:12:41 +0200 |
paulson |
final tidying up of lemma bounded_variation_absolutely_integrable_interval
|
file |
diff |
annotate
|
| Sat, 05 Aug 2017 18:16:35 +0200 |
paulson |
finally rid of finite_product_dependent
|
file |
diff |
annotate
|
| Sat, 05 Aug 2017 16:18:35 +0200 |
paulson |
more cleanup
|
file |
diff |
annotate
|
| Sat, 05 Aug 2017 12:18:25 +0200 |
paulson |
trying to disentangle bounded_variation_absolutely_integrable_interval
|
file |
diff |
annotate
|
| Fri, 04 Aug 2017 21:30:38 +0200 |
paulson |
more horrible proofs disentangled
|
file |
diff |
annotate
|
| Thu, 03 Aug 2017 21:38:05 +0200 |
paulson |
eliminated more "guess", etc.
|
file |
diff |
annotate
|
| Mon, 24 Jul 2017 16:50:46 +0100 |
paulson |
refactored some HORRIBLE integration proofs
|
file |
diff |
annotate
|
| Tue, 27 Jun 2017 15:10:13 +0100 |
paulson |
Removed more "guess", etc.
|
file |
diff |
annotate
|
| Mon, 26 Jun 2017 16:59:44 +0100 |
paulson |
More tidying of horrible proofs
|
file |
diff |
annotate
|
| Mon, 26 Jun 2017 14:26:03 +0100 |
paulson |
A few renamings and several tidied-up proofs
|
file |
diff |
annotate
|
| Thu, 22 Jun 2017 16:31:29 +0100 |
paulson |
New theorems and much tidying up of the old ones
|
file |
diff |
annotate
|