Wed, 14 Nov 2001 18:46:30 +0100 |
wenzelm |
adapted primrec/datatype to Isar;
|
file |
diff |
annotate
|
Fri, 09 Nov 2001 22:53:10 +0100 |
wenzelm |
adapted to add_inductive_x;
|
file |
diff |
annotate
|
Thu, 13 Jul 2000 23:20:57 +0200 |
wenzelm |
adapted PureThy.add_defs_i;
|
file |
diff |
annotate
|
Fri, 05 May 2000 22:37:04 +0200 |
wenzelm |
use Sign.simple_read_term;
|
file |
diff |
annotate
|
Mon, 13 Mar 2000 13:28:31 +0100 |
wenzelm |
adapted to new PureThy.add_thms etc.;
|
file |
diff |
annotate
|
Thu, 13 Jan 2000 17:34:39 +0100 |
paulson |
change in add_thmss to suppress warning
|
file |
diff |
annotate
|
Mon, 04 Oct 1999 21:39:36 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Wed, 27 Jan 1999 15:58:22 +0100 |
paulson |
automatic insertion of datatype intr rules into claset
|
file |
diff |
annotate
|
Tue, 19 Jan 1999 11:18:11 +0100 |
paulson |
removal of the (thm list) argument of mk_cases
|
file |
diff |
annotate
|
Wed, 13 Jan 1999 11:57:09 +0100 |
paulson |
datatype package improvements
|
file |
diff |
annotate
|
Tue, 12 Jan 1999 15:17:37 +0100 |
wenzelm |
eliminated global/local names;
|
file |
diff |
annotate
|
Tue, 12 Jan 1999 13:54:51 +0100 |
wenzelm |
eliminated tthm type and Attribute structure;
|
file |
diff |
annotate
|
Thu, 07 Jan 1999 18:30:55 +0100 |
paulson |
ZF: the natural numbers as a datatype
|
file |
diff |
annotate
|
Wed, 06 Jan 1999 13:24:33 +0100 |
paulson |
induct_tac and exhaust_tac
|
file |
diff |
annotate
|
Mon, 28 Dec 1998 16:58:11 +0100 |
paulson |
revised datatype definition package
|
file |
diff |
annotate
|