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 |