| Sat, 10 Nov 2018 07:57:20 +0000 |
haftmann |
replaced some ancient ASCII syntax
|
file |
diff |
annotate
|
| Mon, 05 Nov 2018 10:02:21 +0100 |
nipkow |
simplified proof, moved lemma, added lemma
|
file |
diff |
annotate
|
| Sat, 27 Oct 2018 15:30:38 +0200 |
nipkow |
moved lemmas
|
file |
diff |
annotate
|
| Thu, 25 Oct 2018 09:48:02 +0000 |
haftmann |
more and generalized lemmas
|
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
|
| Thu, 12 Jul 2018 17:22:39 +0100 |
paulson |
de-applying (mostly Set_Interval)
|
file |
diff |
annotate
|
| Sun, 03 Jun 2018 15:22:30 +0100 |
paulson |
infinite product material
|
file |
diff |
annotate
|
| Wed, 02 May 2018 12:47:56 +0100 |
paulson |
type class generalisations; some work on infinite products
|
file |
diff |
annotate
|
| Sun, 15 Apr 2018 08:32:31 +0000 |
haftmann |
more and generalized lemmas
|
file |
diff |
annotate
|
| Wed, 21 Mar 2018 19:39:23 +0100 |
haftmann |
prefer convention to place operation name before type name
|
file |
diff |
annotate
|
| Sat, 10 Mar 2018 19:36:59 +0000 |
haftmann |
abstract algebraic bit operations
|
file |
diff |
annotate
|
| Mon, 26 Feb 2018 07:34:05 +0100 |
immler |
moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements
|
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
|
| Thu, 15 Feb 2018 12:11:00 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 16 Jan 2018 09:30:00 +0100 |
wenzelm |
standardized towards new-style formal comments: isabelle update_comments;
|
file |
diff |
annotate
|
| Sat, 13 Jan 2018 09:18:54 +0000 |
haftmann |
restored naming of lemmas after corresponding constants
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Mon, 30 Oct 2017 13:18:41 +0000 |
haftmann |
tuned some proofs and added some lemmas
|
file |
diff |
annotate
|
| Mon, 09 Oct 2017 19:10:47 +0200 |
haftmann |
tuned imports
|
file |
diff |
annotate
|
| Wed, 23 Aug 2017 18:28:56 +0200 |
nipkow |
added lemma
|
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
|
| Thu, 16 Mar 2017 13:55:29 +0000 |
paulson |
Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.
|
file |
diff |
annotate
|
| Wed, 04 Jan 2017 16:18:50 +0000 |
paulson |
Many new theorems, and more tidying
|
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
|
| Fri, 30 Sep 2016 14:05:51 +0100 |
paulson |
new material on paths, etc. Also rationalisation
|
file |
diff |
annotate
|
| Thu, 22 Sep 2016 00:12:17 +0200 |
wenzelm |
raw control symbols are superseded by Latex.embed_raw;
|
file |
diff |
annotate
|
| Mon, 19 Sep 2016 20:06:21 +0200 |
fleury |
left_distrib ~> distrib_right, right_distrib ~> distrib_left
|
file |
diff |
annotate
|
| Sun, 18 Sep 2016 20:33:48 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|