[isabelle-dev] HOL-Decision_Procs FAILED
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