| Mon, 28 Aug 2017 20:33:08 +0100 |
paulson |
sorted out cases in negligible_standard_hyperplane
|
file |
diff |
annotate
|
| Mon, 28 Aug 2017 20:02:43 +0100 |
paulson |
Unscrambling continues as far as negligible_standard_hyperplane
|
file |
diff |
annotate
|
| Mon, 28 Aug 2017 16:30:51 +0100 |
paulson |
unscrambled has_integral_restrict_open_subinterval
|
file |
diff |
annotate
|
| Mon, 28 Aug 2017 13:40:41 +0100 |
paulson |
Giant cleanup of fundamental_theorem_of_calculus_interior
|
file |
diff |
annotate
|
| Mon, 28 Aug 2017 00:12:07 +0100 |
paulson |
work on indefinite_integral_continuous_left, etc.
|
file |
diff |
annotate
|
| Sun, 27 Aug 2017 16:17:24 +0100 |
paulson |
some tidying of division_of_nontrivial
|
file |
diff |
annotate
|
| Sun, 27 Aug 2017 13:50:23 +0100 |
paulson |
division_of_nontrivial partial cleanup
|
file |
diff |
annotate
|
| Sat, 26 Aug 2017 23:57:50 +0100 |
paulson |
Elimination of some "presume"
|
file |
diff |
annotate
|
| Sat, 26 Aug 2017 18:04:27 +0100 |
paulson |
unscrambled Henstock_lemma_part1
|
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
|
| Fri, 25 Aug 2017 13:01:01 +0100 |
paulson |
unscrambling of integrable_alt
|
file |
diff |
annotate
|
| Thu, 24 Aug 2017 23:04:33 +0100 |
paulson |
work on integrable_alt, etc.
|
file |
diff |
annotate
|
| Thu, 24 Aug 2017 21:41:13 +0100 |
paulson |
tidying up has_integral'
|
file |
diff |
annotate
|
| Thu, 24 Aug 2017 17:15:53 +0100 |
paulson |
more elimination of "guess", etc.
|
file |
diff |
annotate
|
| Thu, 24 Aug 2017 12:45:46 +0100 |
paulson |
Merge (non-trivial)
|
file |
diff |
annotate
|
| Wed, 23 Aug 2017 23:46:35 +0100 |
paulson |
More tidying, and renaming of theorems
|
file |
diff |
annotate
|
| Wed, 23 Aug 2017 19:54:11 +0100 |
paulson |
More tidying up of monotone_convergence_interval
|
file |
diff |
annotate
|
| Wed, 23 Aug 2017 22:05:53 +0200 |
haftmann |
dedicated local for "operative" avoids namespace pollution
|
file |
diff |
annotate
|
| Wed, 23 Aug 2017 00:38:53 +0100 |
paulson |
more on the dreadful monotone_convergence_interval
|
file |
diff |
annotate
|
| Tue, 15 Aug 2017 18:14:33 +0100 |
paulson |
tidying up henstock_lemma
|
file |
diff |
annotate
|
| Tue, 15 Aug 2017 11:59:14 +0100 |
paulson |
tackling another nightmare proof
|
file |
diff |
annotate
|
| Mon, 14 Aug 2017 19:17:07 +0100 |
paulson |
patching the previous commit
|
file |
diff |
annotate
|
| Mon, 14 Aug 2017 18:54:25 +0100 |
paulson |
further Hensock tidy-up
|
file |
diff |
annotate
|
| Sun, 13 Aug 2017 23:45:45 +0100 |
paulson |
further tidying
|
file |
diff |
annotate
|
| Sun, 13 Aug 2017 19:24:33 +0100 |
paulson |
general rationalisation of Analysis
|
file |
diff |
annotate
|
| Sat, 12 Aug 2017 12:07:47 +0200 |
paulson |
cleanup of integral_norm_bound_integral
|
file |
diff |
annotate
|
| Fri, 11 Aug 2017 23:38:33 +0200 |
paulson |
more Henstock_Kurzweil_Integration cleanup
|
file |
diff |
annotate
|
| Thu, 10 Aug 2017 14:08:09 +0200 |
paulson |
even more horrible proofs disentangled
|
file |
diff |
annotate
|
| Wed, 09 Aug 2017 23:41:47 +0200 |
paulson |
fundamental_theorem_of_calculus_interior: more cleanup
|
file |
diff |
annotate
|
| Wed, 09 Aug 2017 13:41:23 +0200 |
paulson |
more cleanup of fundamental_theorem_of_calculus_interior
|
file |
diff |
annotate
|
| Tue, 08 Aug 2017 23:54:49 +0200 |
paulson |
more cleanup of fundamental_theorem_of_calculus_interior
|
file |
diff |
annotate
|
| Tue, 08 Aug 2017 13:56:29 +0200 |
paulson |
partly unravelled fundamental_theorem_of_calculus_interior
|
file |
diff |
annotate
|
| Tue, 08 Aug 2017 12:37:01 +0200 |
paulson |
more unknotting
|
file |
diff |
annotate
|
| Mon, 07 Aug 2017 12:04:58 +0200 |
paulson |
more Henstock_Kurzweil_Integration cleanup
|
file |
diff |
annotate
|
| Sun, 06 Aug 2017 22:54:03 +0200 |
paulson |
more integration cleanups
|
file |
diff |
annotate
|
| Sun, 06 Aug 2017 11:10:22 +0200 |
paulson |
further cleanup of "guess"
|
file |
diff |
annotate
|
| Sun, 06 Aug 2017 10:41:15 +0200 |
paulson |
towards a cleanup of Henstock_Kurzweil_Integration.thy
|
file |
diff |
annotate
|
| Sun, 30 Jul 2017 21:44:23 +0100 |
paulson |
partial cleanup of the horrible Tagged_Division
|
file |
diff |
annotate
|
| Wed, 26 Jul 2017 16:07:45 +0100 |
paulson |
New theory of Equiintegrability / Continuity of the indefinite integral / improper integration
|
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
|
| Wed, 21 Jun 2017 17:13:55 +0100 |
paulson |
Tidying up integration theory and some new theorems
|
file |
diff |
annotate
|
| Mon, 19 Jun 2017 16:07:47 +0100 |
paulson |
New theorems; stronger theorems; tidier theorems. Also some renaming
|
file |
diff |
annotate
|
| Thu, 15 Jun 2017 17:22:23 +0100 |
paulson |
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
|
file |
diff |
annotate
|
| Tue, 02 May 2017 14:34:06 +0100 |
paulson |
Simplification of some proofs. Also key lemmas using !! rather than ! in premises
|
file |
diff |
annotate
|
| Thu, 27 Apr 2017 15:59:00 +0100 |
paulson |
New material (and some tidying) purely in the Analysis directory
|
file |
diff |
annotate
|
| Tue, 25 Apr 2017 16:39:54 +0100 |
paulson |
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
|
file |
diff |
annotate
|
| Fri, 10 Mar 2017 23:16:40 +0100 |
immler |
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
|
file |
diff |
annotate
|
| Tue, 21 Feb 2017 15:04:01 +0000 |
paulson |
Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion
|
file |
diff |
annotate
|
| Tue, 17 Jan 2017 13:59:10 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Wed, 04 Jan 2017 16:18:50 +0000 |
paulson |
Many new theorems, and more tidying
|
file |
diff |
annotate
|
| Tue, 18 Oct 2016 15:55:53 +0100 |
paulson |
more from moretop.ml
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 17:33:07 +0200 |
nipkow |
setprod -> prod
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
| Thu, 29 Sep 2016 13:02:43 +0200 |
hoelzl |
HOL-Analysis: move gauges and (tagged) divisions to its own theory file
|
file |
diff |
annotate
|
| Wed, 28 Sep 2016 16:15:51 +0200 |
hoelzl |
HOL-Analysis: add cover lemma ported by L. C. Paulson
|
file |
diff |
annotate
|