| Sat, 07 Jul 2018 15:07:37 +0100 |
paulson |
de-applying, etc.
|
file |
diff |
annotate
|
| Wed, 06 Jun 2018 18:19:55 +0200 |
nipkow |
reorient -> split; documented split
|
file |
diff |
annotate
|
| Sun, 20 May 2018 11:57:17 +0200 |
wenzelm |
prefer HTTPS;
|
file |
diff |
annotate
|
| Thu, 03 May 2018 22:34:49 +0100 |
paulson |
Some tidying up (mostly regarding summations from 0)
|
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
|
| Sun, 15 Apr 2018 21:41:40 +0100 |
paulson |
quite a few more results about negligibility, etc., and a bit of tidying up
|
file |
diff |
annotate
|
| Wed, 26 Apr 2017 16:58:31 +0100 |
paulson |
Some fixes related to compactE_image
|
file |
diff |
annotate
|
| Wed, 26 Apr 2017 15:53:35 +0100 |
paulson |
Further new material. The simprule status of some exp and ln identities was reverted.
|
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, 10 Mar 2017 23:16:40 +0100 |
immler |
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 17:33:07 +0200 |
nipkow |
setprod -> prod
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
| Thu, 22 Sep 2016 15:44:47 +0100 |
paulson |
More mainly topological results
|
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
|