[isabelle-dev] Feature suggestion: apply (meth[1!])
makarius at sketis.net
Mon Mar 11 19:58:39 CET 2013
On Mon, 11 Mar 2013, Joachim Breitner wrote:
> This lets you say "assert_goals 5" in your apply scripts where you think
> there should be 5 goals.
Of course there is always a possibility to devise new commands. Critical
review will only start when such things show up in publicly accessible
Isabelle example sessions, or even the main code base.
You can also experiment with something similar as proof method: there is
no problem to emit warnings, and then do nothing. You only need to look
thrice how it generally interacts with the lazy enumeration scheme of goal
states in method expressions (including backtracking).
> If that is not the case, then jEdit shows some red wiggles, but
> otherwise allows you to continue as before.
That aspect is just an accident of the very weak "error recovery" of the
interactive document processing. After the next round of reforms, an
unstructured apply script will stop after the first failed command -- at
that level of nested proof structure.
Getting that right has much higher priority than adding features
More information about the isabelle-dev