[isabelle-dev] HOL-Decision_Procs FAILED

[Gerwin Klein]

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.

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.