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
|