*To*: Julian Brunner <julianbrunner at gmail.com>*Subject*: Re: [isabelle] Isabelle2016-RC0 - default output buffers*From*: Makarius <makarius at sketis.net>*Date*: Fri, 8 Jan 2016 16:33:40 +0100 (CET)*Cc*: "C. Diekmann" <diekmann at in.tum.de>, isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CAE5E_asjxMh1vf8vvdh6qqKOS_KJ=cJEniY_-ufwNEmWvv-aHg@mail.gmail.com>*References*: <CAGbqCMzMMm1=aeuBrHRo5EkgjAB2_v6RCUxNs4DEBJAS=1umjw@mail.gmail.com> <alpine.LNX.2.00.1601032216040.21353@lxbroy10.informatik.tu-muenchen.de> <CAGbqCMxw4Wd6z+Ue=38wwEdNWsE2dHsMP66Yvws9dJN84kkBQA@mail.gmail.com> <CAE5E_asjxMh1vf8vvdh6qqKOS_KJ=cJEniY_-ufwNEmWvv-aHg@mail.gmail.com>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Thu, 7 Jan 2016, Julian Brunner wrote:

My thoughts on the subject: - Interactively viewing the proof state is important to me even though I never write apply-style proofs. When faced with a proof obligation, I like to collect the facts that I think will be relevant with 'using'. This allows me to stare at both the facts and the goal simultaneously in the proof state, getting a better grasp on how to prove the goal. Without the proof state, I would have to restate the facts explicitly in order to view them in close proximity to the goal statement and relieving me of the mental effort of keeping them all in my mind. It also allows me to play around with the facts and the goal in order to get a better idea of the proof. Of course, once found, I may still want to clean up the proof to make it readable without having access to the proof state. - The proof state is also useful when dealing with complex induction rules, relieving me of the mental effort of instantiating the induction rule in my mind and presenting me with nicely formatted subgoals. - Of course, these points do not really apply to educational examples where an experienced user already knows what the proof state is going to be at each point of the proof, as well as which tools will be able to solve which goals. However, they do apply to inexperienced users as well as experienced users working on complex proofs.

- I prefer the 2-buffer model as it takes up less space on my screen without forcing me to switch between two different panels to get various kinds of feedback from the system. It allows me to work with two theories (vertical split), the Theories panel and the Output panel on a single screen (see attached screenshot). When using the 3-buffer model, at most one of the feedback buffers actually provides information most of the time, with the other one just wasting space. However, since it's not always the same feedback buffer that is important, I need to keep both of them open anyways. This problem is made worse by the fact that these panels cannot both be docked at the bottom by default (since these terms can become large, I prefer to have them displayed in a wide rather than a tall buffer). - I prefer touching my mouse as little as possible as I am a fast typist and keeping my hands on the keyboard is usually much more efficient. I feel like hovering the mouse over text in order to get interactive feedback would slow me down significantly.

Makarius

**References**:**Re: [isabelle] Isabelle2016-RC0 - default output buffers***From:*C. Diekmann

**Re: [isabelle] Isabelle2016-RC0 - default output buffers***From:*Makarius

**Re: [isabelle] Isabelle2016-RC0 - default output buffers***From:*C. Diekmann

**Re: [isabelle] Isabelle2016-RC0 - default output buffers***From:*Julian Brunner

- Previous by Date: [isabelle] Code equations for "power"
- Next by Date: Re: [isabelle] Isabelle2016-RC0 - default output buffers
- Previous by Thread: Re: [isabelle] Isabelle2016-RC0 - default output buffers
- Next by Thread: Re: [isabelle] Isabelle2016-RC0 - default output buffers
- Cl-isabelle-users January 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list