| Thu, 31 Jul 2003 00:01:47 +0200 |
berghofe |
Removed extraneous rev in function goal_params (the list of parameters
|
file |
diff |
annotate
|
| Fri, 11 Jul 2003 15:00:10 +0200 |
berghofe |
Exported function goal_params.
|
file |
diff |
annotate
|
| Mon, 03 Feb 2003 11:04:16 +0100 |
berghofe |
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
|
file |
diff |
annotate
|
| Mon, 21 Oct 2002 17:07:27 +0200 |
berghofe |
Removed obsolete functions dealing with flex-flex constraints.
|
file |
diff |
annotate
|
| Wed, 20 Feb 2002 00:53:53 +0100 |
wenzelm |
Symbol.bump_string;
|
file |
diff |
annotate
|
| Thu, 17 Jan 2002 20:59:46 +0100 |
wenzelm |
is_norm_hhf moved to drule.ML;
|
file |
diff |
annotate
|
| Tue, 15 Jan 2002 00:09:54 +0100 |
wenzelm |
added mk_conjunction_list;
|
file |
diff |
annotate
|
| Sun, 11 Nov 2001 21:30:51 +0100 |
wenzelm |
added mk_conjunction;
|
file |
diff |
annotate
|
| Sun, 07 Jan 2001 21:35:34 +0100 |
wenzelm |
added is_norm_hhf;
|
file |
diff |
annotate
|
| Fri, 10 Nov 2000 19:10:34 +0100 |
wenzelm |
has_meta_prems: include "==";
|
file |
diff |
annotate
|
| Thu, 24 Aug 2000 11:14:21 +0200 |
paulson |
fixed strip_assums and assum_pairs, restoring them (essentially) to their
|
file |
diff |
annotate
|
| Mon, 21 Aug 2000 18:16:47 +0200 |
wenzelm |
fixed has_meta_prems: strip_assums_hyp;
|
file |
diff |
annotate
|
| Tue, 01 Aug 2000 00:19:07 +0200 |
wenzelm |
added has_meta_prems;
|
file |
diff |
annotate
|
| Sun, 30 Jul 2000 12:48:55 +0200 |
wenzelm |
Logic.goal_const;
|
file |
diff |
annotate
|
| Wed, 17 Jun 1998 10:48:38 +0200 |
nipkow |
Goals may now contain assumptions, which are not returned.
|
file |
diff |
annotate
|
| Wed, 22 Apr 1998 19:08:49 +0200 |
wenzelm |
added mk_cond_defpair, mk_defpair;
|
file |
diff |
annotate
|
| Mon, 09 Mar 1998 16:09:06 +0100 |
wenzelm |
adapted to baroque chars;
|
file |
diff |
annotate
|
| Wed, 04 Mar 1998 13:16:05 +0100 |
nipkow |
Reorganized simplifier. May now reorient rules.
|
file |
diff |
annotate
|
| Sat, 28 Feb 1998 15:40:03 +0100 |
nipkow |
Tried to reorganize rewriter a little. More to be done.
|
file |
diff |
annotate
|
| Wed, 18 Feb 1998 11:31:25 +0100 |
nipkow |
Improved loop-test for rewrite rules a little.
|
file |
diff |
annotate
|
| Fri, 19 Dec 1997 10:15:51 +0100 |
wenzelm |
term order stuff moved to term.ML;
|
file |
diff |
annotate
|
| Tue, 02 Dec 1997 12:42:28 +0100 |
wenzelm |
tuned term order;
|
file |
diff |
annotate
|
| Fri, 28 Nov 1997 07:35:10 +0100 |
nipkow |
Fixed the definition of `termord': is now antisymmetric.
|
file |
diff |
annotate
|
| Tue, 04 Nov 1997 12:58:10 +0100 |
nipkow |
logic: loops -> rewrite_rule_ok
|
file |
diff |
annotate
|
| Tue, 21 Oct 1997 17:36:54 +0200 |
nipkow |
Corrected alphabetical order of entries in signature.
|
file |
diff |
annotate
|
| Fri, 17 Oct 1997 11:10:13 +0200 |
paulson |
Added "op" before "occs" to make sml/nj happy
|
file |
diff |
annotate
|
| Thu, 16 Oct 1997 13:45:16 +0200 |
nipkow |
The simplifier has been improved a little: equations s=t which used to be
|
file |
diff |
annotate
|
| Thu, 05 Jun 1997 13:30:24 +0200 |
paulson |
Removal of freeze_vars and thaw_vars (quite unused...)
|
file |
diff |
annotate
|
| Thu, 16 Jan 1997 13:44:47 +0100 |
wenzelm |
added term order;
|
file |
diff |
annotate
|
| Thu, 28 Nov 1996 10:44:24 +0100 |
paulson |
Replaced map...~~ by ListPair.map
|
file |
diff |
annotate
|
| Fri, 28 Jun 1996 11:10:32 +0200 |
paulson |
Restored warning comment
|
file |
diff |
annotate
|
| Fri, 16 Feb 1996 12:19:47 +0100 |
paulson |
Elimination of fully-functorial style.
|
file |
diff |
annotate
|
| Mon, 29 Jan 1996 14:16:13 +0100 |
clasohm |
inserted tabs again
|
file |
diff |
annotate
|
| Mon, 29 Jan 1996 13:56:41 +0100 |
clasohm |
removed tabs
|
file |
diff |
annotate
|
| Wed, 12 Oct 1994 16:31:01 +0100 |
wenzelm |
added is_equals: term -> bool;
|
file |
diff |
annotate
|
| Tue, 06 Sep 1994 13:46:53 +0200 |
lcp |
Pure/type/unvarifyT: moved there from logic.ML
|
file |
diff |
annotate
|
| Thu, 18 Aug 1994 17:56:07 +0200 |
lcp |
/unvarifyT, unvarify: moved to Pure/logic.ML
|
file |
diff |
annotate
|
| Wed, 06 Jul 1994 11:36:00 +0200 |
wenzelm |
changed comment only;
|
file |
diff |
annotate
|
| Thu, 26 May 1994 16:40:45 +0200 |
wenzelm |
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
|
file |
diff |
annotate
|
| Tue, 04 Jan 1994 15:48:38 +0100 |
wenzelm |
commented out sig constraint of functor (for debugging purposes);
|
file |
diff |
annotate
|
| Thu, 21 Oct 1993 14:56:12 +0100 |
lcp |
logic/mk_equals,mk_flexpair: now calls fastype_of instead of type_of.
|
file |
diff |
annotate
|
| Thu, 16 Sep 1993 12:20:38 +0200 |
clasohm |
Initial revision
|
file |
diff |
annotate
|