Re: [isabelle] Isabelle2016-RC0 - default output buffers



On Mon, 11 Jan 2016, Tobias Nipkow wrote:

On 09/01/2016 13:21, Makarius wrote:
 On Sat, 9 Jan 2016, Tobias Nipkow wrote:

> >   Can you quote a changeset and mailing list message on that?
> > See
>  https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2015-November/006420.html
>
 That is a rather old thread. I don't see any connection to the way it
 works in
 Isabelle2016-RC0.

Both Cornelius and I refer to the fact that the proof state is not displayed by default in the output window.

The key difference to the version in November 2015:

  * Output has a button to enable "Proof state"

  * State has a button to disable "Auto update"

Thus it is trivial to switch certain modes of operation on the fly.


The State buffer is conceptually cleaner and has many other advantages. The main disadvantage: users need to change old habits, as usual.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.