| Sun, 08 Oct 2017 22:28:21 +0200 |
haftmann |
abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:20 +0200 |
haftmann |
avoid name clashes on interpretation of abstract locales
|
file |
diff |
annotate
|
| Tue, 29 Aug 2017 16:24:14 +0200 |
eberlm |
Some small lemmas about polynomials and FPSs
|
file |
diff |
annotate
|
| Mon, 21 Aug 2017 20:49:15 +0200 |
Manuel Eberl |
HOL-Analysis: Convergent FPS and infinite sums
|
file |
diff |
annotate
|
| Sun, 20 Aug 2017 18:55:03 +0200 |
Manuel Eberl |
More lemmas for HOL-Analysis
|
file |
diff |
annotate
|
| Thu, 03 Aug 2017 13:35:28 +0200 |
eberlm |
Removed unnecessary constant 'ball' from Formal_Power_Series
|
file |
diff |
annotate
|
| Thu, 03 Aug 2017 09:30:09 +0200 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Thu, 15 Jun 2017 17:22:23 +0100 |
paulson |
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
|
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, 07 Apr 2017 21:17:18 +0200 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Thu, 06 Apr 2017 21:37:13 +0200 |
haftmann |
session containing computational algebra
|
file |
diff |
annotate
| base
|