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