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



Personally, I have no problem with the change itself. The new way is cleaner, avoiding mixing error messages with the state output. But it could be disconcerting when encountered for the first time, so we need to advertise it clearly. I have completely switched to the State window and only display the Output window very exceptionally. Other people will do things differently.

Larry

> On 11 Jan 2016, at 17:03, Tobias Nipkow <nipkow at in.tum.de> wrote:
> 
> Both Cornelius and I refer to the fact that the proof state is not displayed by default in the output window.





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