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

2013-03-14 Thread 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

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

2013-03-14 Thread 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.greena...@nicta.com.au wrote: On 08/03/13 23:46, Joachim Breitner wrote: Sometimes, when I’m writing

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

2013-03-14 Thread Makarius
On Thu, 14 Mar 2013, David Greenaway 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

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

2013-03-14 Thread Makarius
On Thu, 14 Mar 2013, Lawrence Paulson wrote: 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. The easily here is ex falso quodlibet consequitur. The system is definitely easy to break by adhoc patching ... Before

[isabelle-dev] Community Involvement in Isabelle Development

2013-03-14 Thread David Greenaway
On 14/03/13 22:37, Makarius wrote: Before we run again into a noisy thread that leads nowhere: the system development process is run by the people doing the actual work. This sounds like a trivial tautology, but is often forgotten. What level of community involvement (i.e., external