Mon, 28 Aug 2017 22:31:47 +0100 |
paulson |
final cleanup of negligible_standard_hyperplane and other things
|
file |
diff |
annotate
|
Fri, 25 Aug 2017 11:10:03 +0100 |
paulson |
renamed s to S to work with previous change
|
file |
diff |
annotate
|
Mon, 24 Jul 2017 16:50:46 +0100 |
paulson |
refactored some HORRIBLE integration proofs
|
file |
diff |
annotate
|
Tue, 18 Jul 2017 11:35:32 +0200 |
eberlm |
poles and residues of the Gamma function
|
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
|
Mon, 19 Jun 2017 16:07:47 +0100 |
paulson |
New theorems; stronger theorems; tidier theorems. Also some renaming
|
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
|
Tue, 21 Feb 2017 17:12:10 +0000 |
paulson |
some new material, also recasting some theorems using “obtains”
|
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
|
Thu, 05 Jan 2017 14:18:24 +0000 |
paulson |
New material about path connectedness, etc.
|
file |
diff |
annotate
|
Wed, 04 Jan 2017 16:18:50 +0000 |
paulson |
Many new theorems, and more tidying
|
file |
diff |
annotate
|
Tue, 03 Jan 2017 16:48:49 +0000 |
paulson |
A few new lemmas and needed adaptations
|
file |
diff |
annotate
|
Tue, 25 Oct 2016 15:46:07 +0100 |
paulson |
more new material
|
file |
diff |
annotate
|
Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
Sun, 16 Oct 2016 09:31:04 +0200 |
haftmann |
more standardized names
|
file |
diff |
annotate
|
Fri, 30 Sep 2016 12:00:17 +0200 |
hoelzl |
HOL-Analysis: move Library/Convex to Convex_Euclidean_Space
|
file |
diff |
annotate
|
Thu, 29 Sep 2016 12:58:55 +0100 |
paulson |
more new material
|
file |
diff |
annotate
|
Thu, 22 Sep 2016 15:44:47 +0100 |
paulson |
More mainly topological results
|
file |
diff |
annotate
|
Wed, 21 Sep 2016 16:59:51 +0100 |
paulson |
new material about topological concepts, etc
|
file |
diff |
annotate
|
Mon, 19 Sep 2016 20:06:21 +0200 |
fleury |
left_distrib ~> distrib_right, right_distrib ~> distrib_left
|
file |
diff |
annotate
|
Mon, 08 Aug 2016 14:13:14 +0200 |
hoelzl |
rename HOL-Multivariate_Analysis to HOL-Analysis.
|
file |
diff |
annotate
| base
|