| Fri, 28 Dec 2018 10:29:59 +0100 |
nipkow |
tuned style and headers
|
file |
diff |
annotate
|
| Thu, 27 Dec 2018 21:00:50 +0100 |
immler |
generalized to big sum
|
file |
diff |
annotate
|
| Thu, 27 Dec 2018 19:48:28 +0100 |
nipkow |
tuned headers; ~ -> \<not>
|
file |
diff |
annotate
|
| Sun, 18 Nov 2018 18:07:51 +0000 |
haftmann |
removed legacy input syntax
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 14:30:09 +0200 |
nipkow |
Prefix form of infix with * on either side no longer needs special treatment
|
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
|
| Sun, 03 Jun 2018 15:22:30 +0100 |
paulson |
infinite product material
|
file |
diff |
annotate
|
| Sun, 20 May 2018 18:37:34 +0100 |
paulson |
tidy up of Derivative
|
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
|
| Sat, 28 Apr 2018 14:38:53 +0100 |
paulson |
getting rid of "defer"
|
file |
diff |
annotate
|
| Thu, 26 Apr 2018 19:51:32 +0200 |
nipkow |
new simp modifier: reorient
|
file |
diff |
annotate
|
| Tue, 17 Apr 2018 22:35:48 +0100 |
paulson |
Change of variables proof
|
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 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
|
| 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
|