[isabelle-dev] HOL-Decision_Procs FAILED

[Lawrence Paulson]

I don’t think this is worth doing.

However some sort of process of identifying and cleaning up horrible old proofs might be worth considering.
Larry

On 18 Mar 2014, at 21:23, Makarius <makarius at sketis.net> wrote:

> Maybe I should try to improve the implicit "rule" method to reveal the rule that was applied --- via a form of semantic completion.  It is a bit more difficult than the other completions so far, because there is also the lazy enumeration of rules and rule instantiations involved.