| Fri, 15 May 1998 11:35:56 +0200 |
wenzelm |
witnesses: lookup stored thms instead of axioms;
|
file |
diff |
annotate
|
| Wed, 13 May 1998 12:17:49 +0200 |
wenzelm |
tuned msg;
|
file |
diff |
annotate
|
| Wed, 29 Apr 1998 11:14:34 +0200 |
wenzelm |
adapted to new PureThy.add_axioms_i;
|
file |
diff |
annotate
|
| Tue, 28 Oct 1997 17:27:10 +0100 |
wenzelm |
add_store_axioms_i;
|
file |
diff |
annotate
|
| Fri, 24 Oct 1997 17:11:48 +0200 |
wenzelm |
removed add_thms_as_axms;
|
file |
diff |
annotate
|
| Mon, 20 Oct 1997 15:20:20 +0200 |
wenzelm |
tuned types;
|
file |
diff |
annotate
|
| Mon, 20 Oct 1997 11:47:04 +0200 |
wenzelm |
fixed goal_XXX;
|
file |
diff |
annotate
|
| Mon, 20 Oct 1997 10:52:32 +0200 |
wenzelm |
fixed types of add_XXX;
|
file |
diff |
annotate
|
| Mon, 13 Oct 1997 17:49:08 +0200 |
wenzelm |
uses Sign.str_of_classrel, Sign.str_of_arity, Sign.str_of_arity;
|
file |
diff |
annotate
|
| Thu, 09 Oct 1997 14:39:44 +0200 |
wenzelm |
fixed axiom names;
|
file |
diff |
annotate
|
| Mon, 06 Oct 1997 18:57:17 +0200 |
wenzelm |
eliminated raise_term, raise_typ;
|
file |
diff |
annotate
|
| Wed, 01 Oct 1997 17:40:09 +0200 |
wenzelm |
fully qualified names: Theory.add_XXX;
|
file |
diff |
annotate
|
| Wed, 06 Aug 1997 15:07:33 +0200 |
wenzelm |
added "Proving ..." msgs;
|
file |
diff |
annotate
|
| Wed, 04 Jun 1997 12:26:42 +0200 |
wenzelm |
eliminated freeze_vars;
|
file |
diff |
annotate
|
| Wed, 16 Apr 1997 18:21:00 +0200 |
wenzelm |
Sorts.str_of_arity;
|
file |
diff |
annotate
|
| Fri, 21 Feb 1997 15:31:47 +0100 |
paulson |
Replaced "flat" by the Basis Library function List.concat
|
file |
diff |
annotate
|
| Thu, 28 Nov 1996 10:44:24 +0100 |
paulson |
Replaced map...~~ by ListPair.map
|
file |
diff |
annotate
|
| Fri, 16 Feb 1996 11:35:52 +0100 |
paulson |
Elimination of fully-functorial style.
|
file |
diff |
annotate
|
| Fri, 01 Sep 1995 13:08:55 +0200 |
wenzelm |
adapted to new version of shyps-stuff;
|
file |
diff |
annotate
|
| Tue, 01 Aug 1995 17:20:21 +0200 |
wenzelm |
modified prep_thm_axm to handle shyps;
|
file |
diff |
annotate
|
| Thu, 27 Jul 1995 13:13:32 +0200 |
wenzelm |
minor fix: instance now raises error if witness axioms don't exist;
|
file |
diff |
annotate
|
| Fri, 27 Jan 1995 13:31:26 +0100 |
wenzelm |
instance: now automatically includes defs of current thy node as witnesses;
|
file |
diff |
annotate
|
| Wed, 12 Oct 1994 16:32:06 +0100 |
wenzelm |
prove_subclass, prove_arity now exported;
|
file |
diff |
annotate
|
| Fri, 19 Aug 1994 15:39:52 +0200 |
wenzelm |
cleaned sig;
|
file |
diff |
annotate
|
| Wed, 27 Jul 1994 15:14:31 +0200 |
wenzelm |
added experimental add_defns (actually should be moved somewhere else);
|
file |
diff |
annotate
|
| Thu, 14 Jul 1994 11:39:25 +0200 |
wenzelm |
added functor signature constraint;
|
file |
diff |
annotate
|
| Wed, 06 Jul 1994 12:49:56 +0200 |
wenzelm |
various minor changes (names and comments);
|
file |
diff |
annotate
|
| Thu, 16 Jun 1994 12:05:53 +0200 |
wenzelm |
(beta release)
|
file |
diff |
annotate
|
| Thu, 26 May 1994 16:53:58 +0200 |
wenzelm |
axiomatic type class 'package' for Pure (alpha version);
|
file |
diff |
annotate
|