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

Makarius makarius at sketis.net
Thu Mar 14 12:37:55 CET 2013

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 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.


More information about the isabelle-dev mailing list