Re: [isabelle] Another newbie question...case-based proofs



Am Montag, den 11.03.2019, 19:24 +0100 schrieb Makarius:
> On 11/03/2019 18:33, Nagashima, Yutaka wrote:
> > Would it be possible to have this "proof state" box ticked by
> > default in the next official Isabelle distribution?
> > It is a small thing that could help new Isabelle users, I think.
>
> I have introduced this default some years ago specifically for new
> users (notable those who have not been spoilt yet by old-style TTY-
> based proof assistants). At the same time I also introduced the State
> dockable as alternative to it.

Until I read your e-mail I hadn’t known that there was a “State
dockable”: the output tab is visible by default, the state dockable is
not.

Now I tried out the State dockable and found that it showed either
nothing or the text that was also shown in the Output tab. Thus I don’t
know currently what the advantage of the State dockable over the Output
tab is.

All the best,
Wolfgang




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