[isabelle-dev] HOL-Decision_Procs FAILED

[Makarius]

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.


 	Makarius