src/Provers/blast.ML
1998-02-25 oheimb 1998-02-25 renamed rep_claset to rep_cs
1998-02-25 oheimb 1998-02-25 changed wrapper mechanism of classical reasoner
1998-01-02 paulson 1998-01-02 Blast_tac now squashes flex-flex pairs immediately
1997-12-23 paulson 1997-12-23 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
1997-12-12 paulson 1997-12-12 More deterministic and therefore faster (sometimes) proof reconstruction
1997-12-03 paulson 1997-12-03 Fixed the treatment of substitution for equations, restricting occurrences of variables on the RHS. Improves performance in many cases, though a few old proofs fail
1997-11-28 paulson 1997-11-28 Printing of statistics including time for search & reconstruction
1997-11-26 paulson 1997-11-26 Statistics
1997-11-21 wenzelm 1997-11-21 changed Pure/Sequence interface -- isatool fixseq;
1997-11-20 paulson 1997-11-20 Renamed "overload" to "overloaded" for sml/nj compatibility
1997-11-17 paulson 1997-11-17 Rationalized error handling: if low-level tactic (depth_tac) cannot accept the goal then it raises exception TRANS. Top-level tactics (blast_tac) generate warnings and then fail immediately.
1997-11-11 paulson 1997-11-11 Now applies "map negOfGoal" to lits when expanding haz rules. Also improved comments
1997-11-05 wenzelm 1997-11-05 fixed exception OPTION;
1997-11-03 wenzelm 1997-11-03 adapted to new implicit claset mechanism;
1997-11-01 paulson 1997-11-01 New treatment of overloading\!
1997-10-17 paulson 1997-10-17 A lot of new comments
1997-07-18 wenzelm 1997-07-18 tuned warning;
1997-06-19 paulson 1997-06-19 Made proofs more concise by replacing calls to spy_analz_tac by uses of analz_insert_eq in rewriting
1997-05-20 paulson 1997-05-20 Basis library version of type "option" now resides in its own structure Option
1997-05-05 paulson 1997-05-05 Again "norm" DOES NOT normalize bodies of abstractions Showterm (used for tracing) now follows variable instantiations (in order to make up for the "norm" change)
1997-05-02 paulson 1997-05-02 More tracing. hyp_subst_tac allowed to fail
1997-04-30 paulson 1997-04-30 More tracing; less exception handling
1997-04-24 wenzelm 1997-04-24 refer to SOME, NONE on top-level;
1997-04-24 paulson 1997-04-24 Addition of printed tracing. Also some tidying
1997-04-23 paulson 1997-04-23 Loop detection: before expanding a haz formula, see whether it is a duplicate and, if so, delete it. Recursion detection: transitivity and similar rules, when applied, put the new formulae at the end of a branch and not at the front (in effect).
1997-04-21 paulson 1997-04-21 Penalty for branching instantiations reduced from log3 to log4. Now allows a branch to close by unifying an OConst with a Const.
1997-04-15 paulson 1997-04-15 Changed penalty from log2 to log3
1997-04-09 paulson 1997-04-09 Control over excessive branching by applying a log2 penalty Incorporation of debugging features Allows backtracking over haz rules if alternatives exist Subsitution for equality may more a rule from the haz to the safe part
1997-04-04 paulson 1997-04-04 Re-organization of the order of haz rules
1997-04-03 paulson 1997-04-03 Now exports declConsts! Temporarily erased target signature to aid debugging
1997-04-02 paulson 1997-04-02 Implementation of blast_tac: fast tableau prover