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



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
> 





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