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



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.