| Fri, 25 Jan 2008 23:05:25 +0100 |
wenzelm |
modernized primrec;
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:23:24 +0200 |
berghofe |
- Renamed inductive2 to inductive
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 20:07:26 +0200 |
wenzelm |
tuned proofs -- avoid implicit prems;
|
file |
diff |
annotate
|
| Wed, 07 Feb 2007 17:44:07 +0100 |
berghofe |
Adapted to new inductive definition package.
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 11:47:57 +0100 |
wenzelm |
renamed 'const_syntax' to 'notation';
|
file |
diff |
annotate
|
| Mon, 11 Sep 2006 21:35:19 +0200 |
wenzelm |
induct method: renamed 'fixing' to 'arbitrary';
|
file |
diff |
annotate
|
| Wed, 09 Aug 2006 00:14:28 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 16 May 2006 21:33:01 +0200 |
wenzelm |
tuned concrete syntax -- abbreviation/const_syntax;
|
file |
diff |
annotate
|
| Sun, 09 Apr 2006 18:51:13 +0200 |
wenzelm |
tuned syntax/abbreviations;
|
file |
diff |
annotate
|
| Sat, 08 Apr 2006 22:51:06 +0200 |
wenzelm |
refined 'abbreviation';
|
file |
diff |
annotate
|
| Thu, 16 Feb 2006 21:12:00 +0100 |
wenzelm |
new-style definitions/abbreviations;
|
file |
diff |
annotate
|
| Fri, 25 Nov 2005 19:09:44 +0100 |
wenzelm |
tuned induct proofs;
|
file |
diff |
annotate
|
| Wed, 23 Nov 2005 22:26:13 +0100 |
wenzelm |
tuned induction proofs;
|
file |
diff |
annotate
|
| Thu, 22 Sep 2005 23:56:15 +0200 |
nipkow |
renamed rules to iprover
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Mon, 11 Oct 2004 07:42:22 +0200 |
nipkow |
Proofs needed to be updated because induction now preserves name of
|
file |
diff |
annotate
|
| Wed, 14 Apr 2004 14:13:05 +0200 |
kleing |
use more symbols in HTML output
|
file |
diff |
annotate
|
| Tue, 24 Jun 2003 10:37:57 +0200 |
berghofe |
Moved strong normalization proof to StrongNorm.thy
|
file |
diff |
annotate
|
| Mon, 30 Sep 2002 15:44:21 +0200 |
nipkow |
modified induct method
|
file |
diff |
annotate
|
| Tue, 13 Nov 2001 22:18:03 +0100 |
wenzelm |
tuned inductions;
|
file |
diff |
annotate
|
| Fri, 09 Nov 2001 00:09:47 +0100 |
wenzelm |
eliminated old "symbols" syntax, use "xsymbols" instead;
|
file |
diff |
annotate
|
| Wed, 31 Oct 2001 22:05:37 +0100 |
wenzelm |
tuned notation (degree instead of dollar);
|
file |
diff |
annotate
|
| Wed, 31 Oct 2001 01:26:42 +0100 |
wenzelm |
(induct set: ...);
|
file |
diff |
annotate
|
| Tue, 30 Oct 2001 17:37:25 +0100 |
wenzelm |
tuned induct proofs;
|
file |
diff |
annotate
|
| Fri, 26 Oct 2001 19:06:53 +0200 |
berghofe |
Eliminated occurrence of rule_format.
|
file |
diff |
annotate
|
| Fri, 26 Oct 2001 16:49:10 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 26 Oct 2001 16:18:14 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 26 Oct 2001 14:22:33 +0200 |
wenzelm |
Rrightarrow;
|
file |
diff |
annotate
|
| Fri, 26 Oct 2001 12:24:19 +0200 |
wenzelm |
tuned notation;
|
file |
diff |
annotate
|
| Thu, 25 Oct 2001 20:04:43 +0200 |
berghofe |
Replaced main proof by proper Isar script.
|
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
|
| Fri, 28 Sep 2001 21:45:11 +0200 |
wenzelm |
inductive: no collective atts;
|
file |
diff |
annotate
|
| Fri, 01 Dec 2000 19:42:05 +0100 |
wenzelm |
schematic goals;
|
file |
diff |
annotate
|
| Wed, 04 Oct 2000 22:21:10 +0200 |
wenzelm |
new 'THEN' syntax;
|
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
|
| Sat, 02 Sep 2000 21:56:24 +0200 |
wenzelm |
HOL/Lambda: converted into new-style theory and document;
|
file |
diff |
annotate
|
| Fri, 01 Sep 2000 00:30:25 +0200 |
wenzelm |
converted Lambda scripts;
|
file |
diff |
annotate
|
| Tue, 29 Aug 2000 00:57:24 +0200 |
wenzelm |
Lambda/InductTermi made new-style theory;
|
file |
diff |
annotate
|
| Sat, 19 Aug 2000 12:47:16 +0200 |
wenzelm |
fixed text;
|
file |
diff |
annotate
|
| Thu, 17 Aug 2000 18:58:49 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 17 Aug 2000 10:34:52 +0200 |
wenzelm |
converted to new-style theory;
|
file |
diff |
annotate
|
| Fri, 23 Jun 2000 12:24:37 +0200 |
berghofe |
Subject reduction and strong normalization of simply-typed lambda terms.
|
file |
diff |
annotate
|