[isabelle-dev] auto quickcheck and auto solve

[Tobias Nipkow]

I have to apologize to Makarius - nothing has been switched off. Why did
I think it had been? Because 2 people (who shall remain nameless)
confirmed it no longer works and they thought it had been switched off.
After I wrote my email - wrong order of events, I agree - I tried it
myself with the release version and it worked fine. (There is a small PG
problem that lead one of the two people to think it did not work, but
that is irrelevant here).

Again, my apologies
Tobias

Am 12/10/2011 16:32, schrieb Tobias Nipkow:
> 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev