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. Larry
On 18 Mar 2014, at 21:23, Makarius <makar...@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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
