| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Mon, 24 Jan 2005 18:12:22 +0100 |
berghofe |
Replaced xstring by thmref.
|
file |
diff |
annotate
|
| Wed, 15 May 2002 10:44:58 +0200 |
paulson |
better error messages for datatypes not declared Const
|
file |
diff |
annotate
|
| Tue, 12 Feb 2002 20:28:27 +0100 |
wenzelm |
got rid of explicit marginal comments (now stripped earlier from input);
|
file |
diff |
annotate
|
| Mon, 19 Nov 2001 20:47:57 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 16 Nov 2001 22:08:55 +0100 |
wenzelm |
additional P.marg_comment;
|
file |
diff |
annotate
|
| Wed, 14 Nov 2001 23:18:13 +0100 |
wenzelm |
use proper intr_names (for required case_names);
|
file |
diff |
annotate
|
| 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
|