| Thu, 14 Jul 2005 19:28:29 +0200 |
wenzelm |
occs no longer infix (structure not open);
|
file |
diff |
annotate
|
| Tue, 31 May 2005 11:53:21 +0200 |
wenzelm |
added nth_prem;
|
file |
diff |
annotate
|
| Wed, 09 Mar 2005 18:44:52 +0100 |
ballarin |
First version of global registration command.
|
file |
diff |
annotate
|
| Mon, 24 Jan 2005 12:41:06 +0100 |
paulson |
thin_tac now works on P==>Q
|
file |
diff |
annotate
|
| Fri, 21 Jan 2005 13:55:07 +0100 |
paulson |
fixed thin_tac with higher-level assumptions by removing the old code to
|
file |
diff |
annotate
|
| 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
|