[isabelle-dev] HOL-Decision_Procs FAILED

Lawrence Paulson lp15 at cam.ac.uk
Wed Mar 19 12:49:27 CET 2014

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.

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.

More information about the isabelle-dev mailing list