| Wed, 29 Dec 2010 17:34:41 +0100 |
wenzelm |
explicit file specifications -- avoid secondary load path;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 17:05:57 +0100 |
krauss |
more recdef (and old primrec) hunting
|
file |
diff |
annotate
|
| Sun, 10 Jan 2010 18:43:45 +0100 |
berghofe |
Adapted to changes in induct method.
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 19:36:52 +0200 |
wenzelm |
tuned header;
|
file |
diff |
annotate
|
| Wed, 18 Feb 2009 07:24:13 -0800 |
huffman |
speed up proof of exp_exists
|
file |
diff |
annotate
|
| Mon, 01 Sep 2008 19:17:47 +0200 |
nipkow |
renamed lemma
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 18:30:11 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Sun, 03 Jun 2007 23:16:47 +0200 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Mon, 11 Sep 2006 21:35:19 +0200 |
wenzelm |
induct method: renamed 'fixing' to 'arbitrary';
|
file |
diff |
annotate
|
| Sat, 27 May 2006 17:42:02 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 17 Mar 2006 10:04:27 +0100 |
ballarin |
Renamed setsum_mult to setsum_right_distrib.
|
file |
diff |
annotate
|
| Mon, 20 Feb 2006 21:51:50 +0100 |
kleing |
fixed
|
file |
diff |
annotate
|
| Sun, 19 Feb 2006 13:21:32 +0100 |
kleing |
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
|
file |
diff |
annotate
|
| Sun, 12 Feb 2006 21:34:20 +0100 |
wenzelm |
minor tuning of proofs, notably induct;
|
file |
diff |
annotate
|
| Sun, 12 Feb 2006 10:42:19 +0100 |
kleing |
* moved ThreeDivides from Isar_examples to better suited HOL/ex
|
file |
diff |
annotate
|