| 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
|