*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Another newbie question...case-based proofs*From*: "Eugene W. Stark" <isabelle-users at starkeffect.com>*Date*: Mon, 11 Mar 2019 14:27:56 -0400*In-reply-to*: <52058e21-3316-653f-0fa7-ec3f1f56c1a6@sketis.net>*References*: <CAJ=ZMJK4d0xDP4ULTqEFWwXcHdfPN4yLVqRdPV_nht9VHAWbkQ@mail.gmail.com> <2315a38013d645bfa7ed4a7a37948817@chalmers.se> <D296D69F59ADF247B47C452A21D6ED2314142FD6@XMBX3.uibk.ac.at> <52058e21-3316-653f-0fa7-ec3f1f56c1a6@sketis.net>*Reply-to*: stark at cs.stonybrook.edu*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.5.1

The output panel is the most useful panel in the entire display. Maybe even more useful than the source panel. - Gene Stark On 3/11/19 2:24 PM, Makarius wrote: > On 11/03/2019 18:33, Nagashima, Yutaka wrote: >> >>> One more note on your email, if you tick the "Proof state" box in the output panel, >>> you'll see that parser for structure proofs alternates >>> between "proof (state)" mode and "proof (prove)" mode. >> >> 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. Current users can rather trivially arrange their > default GUI for the preferred setup: either old-style Output with proof > state enabled, or new-style State which is specifically for the proof state. > > I've given several 1-2 day courses of Isabelle where the first 1/2 day > worked very well without ever showing Output or its old-fashioned proof > state within it. Recall that Isabelle/Isar is about proof documents, not > "proof scripts". So there is one main document editor where you compose > your text; everything else is somewhere in the background. > > Further note that the State panel has various technological advantages > over implicit output of states via the Output panel: the State GUI can > interact more directly with the prover, without requiring changes to > commands in the text. In the next round of refinement, the State panel > will get more buttons and options to help interactive development of > proof documents in the main buffer. > > The optional proof state in the Output panel will not participate in > further upgrades, and might eventually fall out of use. > > > Makarius >

**References**:**[isabelle] Another newbie question...case-based proofs***From:*John F. Hughes

**Re: [isabelle] Another newbie question...case-based proofs***From:*Thomas Sewell

**Re: [isabelle] Another newbie question...case-based proofs***From:*Nagashima, Yutaka

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

- Previous by Date: Re: [isabelle] Another newbie question...case-based proofs
- Next by Date: Re: [isabelle] Another newbie question...case-based proofs
- Previous by Thread: Re: [isabelle] Another newbie question...case-based proofs
- Next by Thread: Re: [isabelle] Another newbie question...case-based proofs
- Cl-isabelle-users March 2019 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