| 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 |