Fri, 04 Oct 2002 15:23:58 +0200 |
paulson |
Fixed bug involving inductive definitions with equalities in the premises.
|
file |
diff |
annotate
|
Wed, 20 Feb 2002 00:53:53 +0100 |
wenzelm |
Symbol.bump_string;
|
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
|
Sat, 12 Jan 2002 16:37:58 +0100 |
wenzelm |
renamed forall_elim_vars_safe to gen_all;
|
file |
diff |
annotate
|
Fri, 11 Jan 2002 14:53:30 +0100 |
wenzelm |
replace gen_all by forall_elim_vars_safe;
|
file |
diff |
annotate
|
Mon, 19 Nov 2001 20:47:57 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 16 Nov 2001 22:09:44 +0100 |
wenzelm |
actually store "coinduct" rule;
|
file |
diff |
annotate
|
Wed, 14 Nov 2001 23:20:41 +0100 |
wenzelm |
case_names;
|
file |
diff |
annotate
|
Wed, 14 Nov 2001 18:46:30 +0100 |
wenzelm |
adapted primrec/datatype to Isar;
|
file |
diff |
annotate
|
Tue, 13 Nov 2001 22:20:51 +0100 |
wenzelm |
rearranged inductive package for Isar;
|
file |
diff |
annotate
|
Fri, 09 Nov 2001 22:53:41 +0100 |
wenzelm |
support co/inductive definitions in new-style theories;
|
file |
diff |
annotate
|
Thu, 04 Oct 2001 15:29:37 +0200 |
wenzelm |
qualify MetaSimplifier;
|
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
|
Mon, 04 Oct 1999 21:39:10 +0200 |
wenzelm |
mk_frees, assume_read moved here;
|
file |
diff |
annotate
|
Tue, 21 Sep 1999 19:11:07 +0200 |
nipkow |
Mod because of new solver interface.
|
file |
diff |
annotate
|
Wed, 03 Feb 1999 13:29:24 +0100 |
paulson |
standard spelling: type-checking
|
file |
diff |
annotate
|
Tue, 19 Jan 1999 11:18:11 +0100 |
paulson |
removal of the (thm list) argument of mk_cases
|
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
|
Mon, 28 Dec 1998 16:58:00 +0100 |
paulson |
revised inductive definition package
|
file |
diff |
annotate
|