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

[Lawrence Paulson]

I agree with you, and it seems a mistake to expect jEdit to do all kinds of things that could very easily be done otherwise.

Larry

On 14 Mar 2013, at 07:57, David Greenaway <david.greenaway at nicta.com.au> wrote:

> 
> 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.
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev