| Wed, 12 May 1999 17:26:56 +0200 | wenzelm | strip_quotes replaced by unenclose; | file | diff | annotate |
| Tue, 04 May 1999 16:18:16 +0200 | wenzelm | add_recdef: removed names / attributes; | file | diff | annotate |
| Fri, 30 Apr 1999 18:09:33 +0200 | wenzelm | separated recdef / defer_recdef; | file | diff | annotate |
| Tue, 27 Apr 1999 10:51:16 +0200 | wenzelm | adapted add_inductive, add_record; | file | diff | annotate |
| Fri, 23 Apr 1999 12:22:30 +0200 | paulson | Now for recdefs that omit the WF relation | file | diff | annotate |
| Thu, 22 Apr 1999 12:49:34 +0200 | wenzelm | recdef adapted to RecdefPackage.add_recdef; | file | diff | annotate |
| Wed, 14 Apr 1999 14:44:04 +0200 | wenzelm | intrs: names and atts; | file | diff | annotate |
| Wed, 17 Mar 1999 13:47:04 +0100 | wenzelm | adapted rep_datatype; | file | diff | annotate |
| Thu, 11 Mar 1999 21:56:22 +0100 | wenzelm | primrec: empty attributes; | file | diff | annotate |
| Tue, 12 Jan 1999 16:42:21 +0100 | wenzelm | get_tthms witness theorems; | file | diff | annotate |
| Mon, 28 Dec 1998 16:46:15 +0100 | paulson | replaced obsolete "trim" by "strip_quotes" | file | diff | annotate |
| Wed, 21 Oct 1998 17:46:00 +0200 | berghofe | Changed syntax of rep_datatype and inductive: Theorems | file | diff | annotate |
| Fri, 16 Oct 1998 18:50:20 +0200 | berghofe | Changed structure of name spaces for datatypes. | file | diff | annotate |
| Thu, 30 Jul 1998 23:14:41 +0200 | berghofe | Fixed primrec. | file | diff | annotate |
| Thu, 30 Jul 1998 22:58:05 +0200 | berghofe | Fixed primrec. | file | diff | annotate |
| Thu, 30 Jul 1998 17:59:57 +0200 | wenzelm | fixed primrec; | file | diff | annotate |
| Fri, 24 Jul 1998 13:03:20 +0200 | berghofe | Adapted to new datatype package. | file | diff | annotate |
| Tue, 30 Jun 1998 20:42:47 +0200 | berghofe | Adapted to new inductive definition package. | file | diff | annotate |
| Wed, 29 Apr 1998 11:44:30 +0200 | wenzelm | TypedefPackage.add_typedef; | file | diff | annotate |
| Thu, 08 Jan 1998 18:09:47 +0100 | oheimb | added split_paired_Ex to the implicit simpset | file | diff | annotate |
| Thu, 13 Nov 1997 15:14:14 +0100 | wenzelm | fixed record parser; | file | diff | annotate |
| Thu, 13 Nov 1997 12:43:17 +0100 | wenzelm | improved record syntax; | file | diff | annotate |
| Wed, 12 Nov 1997 12:24:55 +0100 | oheimb | renamed split_T_case_prem to split_T_case_asm | file | diff | annotate |
| Fri, 07 Nov 1997 08:25:02 +0100 | nipkow | Each datatype t now proves a theorem split_t_case_prem | file | diff | annotate |
| Mon, 03 Nov 1997 21:13:24 +0100 | wenzelm | tuned; | file | diff | annotate |
| Mon, 03 Nov 1997 12:24:13 +0100 | wenzelm | isatool fixclasimp; | file | diff | annotate |
| Thu, 30 Oct 1997 09:45:03 +0100 | nipkow | For each datatype `t' there is now a theorem `split_t_case' of the form | file | diff | annotate |
| Fri, 24 Oct 1997 17:28:20 +0200 | wenzelm | record: tuned output; | file | diff | annotate |
| Thu, 23 Oct 1997 12:49:16 +0200 | wenzelm | added record section; | file | diff | annotate |
| Mon, 20 Oct 1997 11:14:55 +0200 | wenzelm | adapted to qualified names; | file | diff | annotate |