| Thu, 14 Jul 2005 19:28:40 +0200 |
wenzelm |
no open Logic;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 18:33:42 +0200 |
wenzelm |
Context.names_of;
|
file |
diff |
annotate
|
| Wed, 13 Apr 2005 18:45:25 +0200 |
wenzelm |
*** MESSAGE REFERS TO PREVIOUS VERSION ***
|
file |
diff |
annotate
|
| Wed, 13 Apr 2005 18:34:22 +0200 |
wenzelm |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 04 Mar 2005 15:07:34 +0100 |
skalberg |
Removed practically all references to Library.foldr.
|
file |
diff |
annotate
|
| 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
|
| Thu, 12 Dec 2002 11:38:18 +0100 |
paulson |
Better treatment of equality in premises of inductive definitions. Less
|
file |
diff |
annotate
|
| 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
|