Fri, 01 Sep 2000 00:36:08 +0200 |
wenzelm |
Method.bang_sectioned_args';
|
file |
diff |
annotate
|
Tue, 01 Aug 2000 11:57:09 +0200 |
wenzelm |
handle actual object-logic rules by atomizing the goal;
|
file |
diff |
annotate
|
Wed, 28 Jun 2000 10:54:47 +0200 |
paulson |
warns of weak elim rules and ignores them
|
file |
diff |
annotate
|
Sat, 25 Sep 1999 13:23:58 +0200 |
wenzelm |
simplified sectioned_args;
|
file |
diff |
annotate
|
Tue, 21 Sep 1999 17:26:50 +0200 |
wenzelm |
setup for refined facts handling;
|
file |
diff |
annotate
|
Wed, 18 Aug 1999 20:47:31 +0200 |
wenzelm |
Method.modifier;
|
file |
diff |
annotate
|
Mon, 02 Aug 1999 17:59:25 +0200 |
wenzelm |
blast method: optional depth argument;
|
file |
diff |
annotate
|
Wed, 14 Jul 1999 13:05:46 +0200 |
wenzelm |
improved comment;
|
file |
diff |
annotate
|
Fri, 09 Jul 1999 18:54:55 +0200 |
wenzelm |
type claset: added extra I/E rules;
|
file |
diff |
annotate
|
Wed, 17 Mar 1999 16:33:47 +0100 |
wenzelm |
Theory.sign_of;
|
file |
diff |
annotate
|
Wed, 25 Nov 1998 14:03:20 +0100 |
wenzelm |
replaced prs by std_output / writeln;
|
file |
diff |
annotate
|
Wed, 18 Nov 1998 11:01:48 +0100 |
wenzelm |
method setup;
|
file |
diff |
annotate
|
Fri, 23 Oct 1998 11:03:35 +0200 |
paulson |
occurs check now handles Bound variables (for soundness)
|
file |
diff |
annotate
|
Mon, 05 Oct 1998 10:30:57 +0200 |
paulson |
MLWorks demands the "op" before $
|
file |
diff |
annotate
|
Fri, 11 Sep 1998 16:31:40 +0200 |
paulson |
Less deterministic reconstruction: now more robust but perhaps slower
|
file |
diff |
annotate
|
Thu, 10 Sep 1998 17:33:09 +0200 |
paulson |
Allows more backtracking in proof reconstruction, making it slower but more
|
file |
diff |
annotate
|
Tue, 01 Sep 1998 10:10:27 +0200 |
paulson |
fixed error msg
|
file |
diff |
annotate
|
Wed, 19 Aug 1998 10:49:30 +0200 |
paulson |
new version, more resistant to PROOF FAILED. Now it distinguishes between
|
file |
diff |
annotate
|
Wed, 25 Feb 1998 20:29:58 +0100 |
oheimb |
renamed rep_claset to rep_cs
|
file |
diff |
annotate
|
Wed, 25 Feb 1998 15:51:24 +0100 |
oheimb |
changed wrapper mechanism of classical reasoner
|
file |
diff |
annotate
|
Fri, 02 Jan 1998 17:16:39 +0100 |
paulson |
Blast_tac now squashes flex-flex pairs immediately
|
file |
diff |
annotate
|
Tue, 23 Dec 1997 11:39:03 +0100 |
paulson |
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
|
file |
diff |
annotate
|
Fri, 12 Dec 1997 10:34:21 +0100 |
paulson |
More deterministic and therefore faster (sometimes) proof reconstruction
|
file |
diff |
annotate
|
Wed, 03 Dec 1997 11:42:45 +0100 |
paulson |
Fixed the treatment of substitution for equations, restricting occurrences of
|
file |
diff |
annotate
|
Fri, 28 Nov 1997 10:52:04 +0100 |
paulson |
Printing of statistics including time for search & reconstruction
|
file |
diff |
annotate
|
Wed, 26 Nov 1997 16:49:54 +0100 |
paulson |
Statistics
|
file |
diff |
annotate
|
Fri, 21 Nov 1997 15:29:56 +0100 |
wenzelm |
changed Pure/Sequence interface -- isatool fixseq;
|
file |
diff |
annotate
|
Thu, 20 Nov 1997 10:54:04 +0100 |
paulson |
Renamed "overload" to "overloaded" for sml/nj compatibility
|
file |
diff |
annotate
|
Mon, 17 Nov 1997 10:48:07 +0100 |
paulson |
Rationalized error handling: if low-level tactic (depth_tac) cannot accept the
|
file |
diff |
annotate
|
Tue, 11 Nov 1997 11:12:37 +0100 |
paulson |
Now applies "map negOfGoal" to lits when expanding haz rules.
|
file |
diff |
annotate
|