[isabelle-dev] auto quickcheck and auto solve

Tobias Nipkow nipkow at in.tum.de
Wed Oct 12 16:32:02 CEST 2011


I find it very objectionable that the new release does no longer support
these two auto features in Proof General. They are part of ongoing
research in Munich and are appreciated by many users. If you do not know
how to make them work with jedit, this is no reason to disable them
under Proof General. Isabelle is a joint project and such wide-ranging
changes must be discussed beforehand. Can you put them back to allow
users of the development version to be as productive as before?

Tobias


More information about the isabelle-dev mailing list