| Mon, 09 Oct 2017 15:34:23 +0100 |
paulson |
new material about connectedness, etc.
|
file |
diff |
annotate
|
| Tue, 19 Sep 2017 16:37:19 +0100 |
paulson |
Using the "constant_on" operator
|
file |
diff |
annotate
|
| Tue, 22 Aug 2017 21:36:48 +0200 |
Manuel Eberl |
Lemmas about analysis and permutations
|
file |
diff |
annotate
|
| Sun, 20 Aug 2017 03:35:20 +0200 |
Manuel Eberl |
Various lemmas for HOL-Analysis
|
file |
diff |
annotate
|
| Fri, 11 Aug 2017 14:29:30 +0200 |
eberlm |
Some facts about orders of zeros
|
file |
diff |
annotate
|
| Tue, 18 Jul 2017 11:35:32 +0200 |
eberlm |
poles and residues of the Gamma function
|
file |
diff |
annotate
|
| Tue, 30 May 2017 14:04:48 +0200 |
nipkow |
tuned names
|
file |
diff |
annotate
|
| Tue, 30 May 2017 10:03:35 +0200 |
nipkow |
redefined Greatest
|
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
|
| Fri, 21 Apr 2017 16:48:58 +0200 |
wenzelm |
tuned imports;
|
file |
diff |
annotate
|
| Tue, 28 Feb 2017 13:51:47 +0000 |
paulson |
Renamed ii to imaginary_unit in order to free up ii as a variable name. Also replaced some legacy def commands
|
file |
diff |
annotate
|
| Wed, 22 Feb 2017 15:04:59 +0000 |
paulson |
New theory about Winding Numbers
|
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
|
| 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
|
| 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
|