[isabelle-dev] HOL-Decision_Procs FAILED
makarius at sketis.net
Tue Mar 18 22:23:13 CET 2014
On Tue, 18 Mar 2014, Lawrence Paulson wrote:
> I may partly be to blame by introducing some metis calls. But there are
> some terrible proofs here (e.g. just “rule”, WTF?).
I see that everybody is happily cleaning up these slightly odd theories
due to Robert Himmelmann, based on material from John Harrison.
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