| Wed, 30 Aug 2017 21:46:41 +0100 |
paulson |
unscrambled has_integral_Union
|
file |
diff |
annotate
|
| Tue, 29 Aug 2017 17:41:11 +0100 |
paulson |
last-minute integration unscrambling
|
file |
diff |
annotate
|
| Mon, 28 Aug 2017 22:31:47 +0100 |
paulson |
final cleanup of negligible_standard_hyperplane and other things
|
file |
diff |
annotate
|
| 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
|