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_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
