| Sat, 14 Apr 2018 09:23:00 +0100 |
paulson |
new material about vec, real^1, etc.
|
file |
diff |
annotate
|
| Mon, 09 Apr 2018 17:21:10 +0100 |
paulson |
merged
|
file |
diff |
annotate
|
| Mon, 09 Apr 2018 17:20:58 +0100 |
paulson |
A couple of new results
|
file |
diff |
annotate
|
| Mon, 09 Apr 2018 16:20:23 +0200 |
nipkow |
removed dots at the end of (sub)titles
|
file |
diff |
annotate
|
| Sun, 25 Feb 2018 12:54:55 +0000 |
paulson |
new material on matrices, etc., and consolidating duplicate results about of_nat
|
file |
diff |
annotate
|
| Thu, 22 Feb 2018 18:01:08 +0100 |
immler |
merged
|
file |
diff |
annotate
|
| Thu, 22 Feb 2018 15:17:25 +0100 |
immler |
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
|
file |
diff |
annotate
|
| Wed, 21 Feb 2018 12:57:49 +0000 |
paulson |
Lots of new material about matrices, etc.
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Mon, 08 Jan 2018 17:11:25 +0000 |
paulson |
moved in some material from Euler-MacLaurin
|
file |
diff |
annotate
|
| Thu, 19 Oct 2017 17:16:01 +0100 |
paulson |
Switching to inverse image and constant_on, plus some new material
|
file |
diff |
annotate
|
| Mon, 09 Oct 2017 15:34:23 +0100 |
paulson |
new material about connectedness, etc.
|
file |
diff |
annotate
|
| Fri, 29 Sep 2017 14:17:17 +0100 |
paulson |
Merge (resolved trivial conflict)
|
file |
diff |
annotate
|
| Fri, 29 Sep 2017 14:12:14 +0100 |
paulson |
New results for Green's theorem
|
file |
diff |
annotate
|
| Thu, 31 Aug 2017 18:30:18 +0100 |
paulson |
more proof simplificaition
|
file |
diff |
annotate
|
| Wed, 30 Aug 2017 22:51:30 +0100 |
paulson |
eliminated some goal_cases
|
file |
diff |
annotate
|
| 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
|
| 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
|