| 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
|
| Wed, 05 Nov 1997 11:45:51 +0100 |
wenzelm |
fixed exception OPTION;
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 11:56:17 +0100 |
wenzelm |
adapted to new implicit claset mechanism;
|
file |
diff |
annotate
|
| Sat, 01 Nov 1997 13:02:39 +0100 |
paulson |
New treatment of overloading\!
|
file |
diff |
annotate
|
| Fri, 17 Oct 1997 11:12:36 +0200 |
paulson |
A lot of new comments
|
file |
diff |
annotate
|
| Fri, 18 Jul 1997 13:54:41 +0200 |
wenzelm |
tuned warning;
|
file |
diff |
annotate
|
| Thu, 19 Jun 1997 11:31:14 +0200 |
paulson |
Made proofs more concise by replacing calls to spy_analz_tac by uses of
|
file |
diff |
annotate
|
| Tue, 20 May 1997 11:47:33 +0200 |
paulson |
Basis library version of type "option" now resides in its own structure Option
|
file |
diff |
annotate
|
| Mon, 05 May 1997 12:15:20 +0200 |
paulson |
Again "norm" DOES NOT normalize bodies of abstractions
|
file |
diff |
annotate
|
| Fri, 02 May 1997 10:18:50 +0200 |
paulson |
More tracing. hyp_subst_tac allowed to fail
|
file |
diff |
annotate
|
| Wed, 30 Apr 1997 12:59:24 +0200 |
paulson |
More tracing; less exception handling
|
file |
diff |
annotate
|
| Thu, 24 Apr 1997 19:47:53 +0200 |
wenzelm |
refer to SOME, NONE on top-level;
|
file |
diff |
annotate
|
| Thu, 24 Apr 1997 11:21:46 +0200 |
paulson |
Addition of printed tracing. Also some tidying
|
file |
diff |
annotate
|
| Wed, 23 Apr 1997 11:11:38 +0200 |
paulson |
Loop detection: before expanding a haz formula, see whether it is a duplicate
|
file |
diff |
annotate
|
| Mon, 21 Apr 1997 10:16:01 +0200 |
paulson |
Penalty for branching instantiations reduced from log3 to log4.
|
file |
diff |
annotate
|
| Tue, 15 Apr 1997 10:22:50 +0200 |
paulson |
Changed penalty from log2 to log3
|
file |
diff |
annotate
|
| Wed, 09 Apr 1997 12:36:52 +0200 |
paulson |
Control over excessive branching by applying a log2 penalty
|
file |
diff |
annotate
|
| Fri, 04 Apr 1997 11:28:28 +0200 |
paulson |
Re-organization of the order of haz rules
|
file |
diff |
annotate
|
| Thu, 03 Apr 1997 10:32:34 +0200 |
paulson |
Now exports declConsts!
|
file |
diff |
annotate
|
| Wed, 02 Apr 1997 11:15:46 +0200 |
paulson |
Implementation of blast_tac: fast tableau prover
|
file |
diff |
annotate
|