[isabelle-dev] Feature suggestion: apply (meth[1!])

[David Greenaway]

On 08/03/13 23:46, Joachim Breitner wrote:
> Sometimes, when I’m writing apply-script style proofs, I have wanted
> a way to modify a proof method foo to “Try foo on the first goal. If
> it solves the goal, good, if it does not solve it, fail”.
[...]
> I wanted to see if I could implement such a feature myself and came up
> with the attached patch – maybe it is already sufficient?

Sorry to raise this thread again, but what was the outcome of this
patch?

Was the general concept of a "solve" tactical rejected, or just the
particular choice of syntax / implementation? (If so, how could it be
improved?) Or have the core developers just been busy? (I apologise if
so!)

I know that the conversion moved on how jEdit might additionally assist
users in determining where a proof script became broken, but I didn't
come to understand why this simple patch would be mutually exclusive to
other more elaborate options.

Cheers,
David


________________________________

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.