src/Provers/blast.ML
Fri, 18 Jul 1997 13:54:41 +0200 wenzelm tuned warning;
Thu, 19 Jun 1997 11:31:14 +0200 paulson Made proofs more concise by replacing calls to spy_analz_tac by uses of
Tue, 20 May 1997 11:47:33 +0200 paulson Basis library version of type "option" now resides in its own structure Option
Mon, 05 May 1997 12:15:20 +0200 paulson Again "norm" DOES NOT normalize bodies of abstractions
Fri, 02 May 1997 10:18:50 +0200 paulson More tracing. hyp_subst_tac allowed to fail
Wed, 30 Apr 1997 12:59:24 +0200 paulson More tracing; less exception handling
Thu, 24 Apr 1997 19:47:53 +0200 wenzelm refer to SOME, NONE on top-level;
Thu, 24 Apr 1997 11:21:46 +0200 paulson Addition of printed tracing. Also some tidying
Wed, 23 Apr 1997 11:11:38 +0200 paulson Loop detection: before expanding a haz formula, see whether it is a duplicate
Mon, 21 Apr 1997 10:16:01 +0200 paulson Penalty for branching instantiations reduced from log3 to log4.
Tue, 15 Apr 1997 10:22:50 +0200 paulson Changed penalty from log2 to log3
Wed, 09 Apr 1997 12:36:52 +0200 paulson Control over excessive branching by applying a log2 penalty
Fri, 04 Apr 1997 11:28:28 +0200 paulson Re-organization of the order of haz rules
Thu, 03 Apr 1997 10:32:34 +0200 paulson Now exports declConsts!
Wed, 02 Apr 1997 11:15:46 +0200 paulson Implementation of blast_tac: fast tableau prover
less more (0) tip