| Wed, 13 Jun 2007 18:30:11 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Wed, 07 Feb 2007 17:46:03 +0100 |
berghofe |
Adapted to changes in Finite_Set theory.
|
file |
diff |
annotate
|
| Wed, 23 Nov 2005 22:26:13 +0100 |
wenzelm |
tuned induction proofs;
|
file |
diff |
annotate
|
| Wed, 16 Nov 2005 17:50:35 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 10 Nov 2005 21:14:05 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Thu, 30 May 2002 10:12:52 +0200 |
nipkow |
Modifications due to enhanced linear arithmetic.
|
file |
diff |
annotate
|
| Tue, 30 Oct 2001 17:37:25 +0100 |
wenzelm |
tuned induct proofs;
|
file |
diff |
annotate
|
| Sat, 06 Oct 2001 00:02:46 +0200 |
wenzelm |
* sane numerals (stage 2): plain "num" syntax (removed "#");
|
file |
diff |
annotate
|
| Fri, 05 Oct 2001 21:52:39 +0200 |
wenzelm |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
|
file |
diff |
annotate
|
| Mon, 06 Nov 2000 22:56:07 +0100 |
wenzelm |
improved: 'induct' handle non-atomic goals;
|
file |
diff |
annotate
|
| Fri, 03 Nov 2000 21:33:53 +0100 |
wenzelm |
adapted "obtain" proofs;
|
file |
diff |
annotate
|
| Sun, 17 Sep 2000 22:19:02 +0200 |
wenzelm |
isar-strip-terminators;
|
file |
diff |
annotate
|
| Tue, 12 Sep 2000 22:13:23 +0200 |
wenzelm |
renamed atts: rulify to rule_format, elimify to elim_format;
|
file |
diff |
annotate
|
| Thu, 07 Sep 2000 21:10:11 +0200 |
wenzelm |
updated attribute names;
|
file |
diff |
annotate
|