[isabelle-dev] HOL-Decision_Procs FAILED

Gerwin Klein Gerwin.Klein at nicta.com.au
Wed Mar 19 13:26:40 CET 2014

On 18 Mar 2014, at 10:23 pm, Makarius <makarius at 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.



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.

More information about the isabelle-dev mailing list