On 18 Mar 2014, at 10:23 pm, 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.
I think beginners would like that, although it does sound like potential for a fairly deep rabbit hole. Gerwin ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
