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



On 12/03/2019 12:18, Lawrence Paulson wrote:
> I only use the output panel for one thing: the “explore” tool. (A very useful add-on: it transforms your current proof state into explicit Isar text for writing your structured proof.) That’s because the formatting is better from the output panel. I certainly hope that “explore” will find its way into a release soon.

See Isabelle2091-RC0/src/HOL/ex/Sketch_and_Explore.thy with these
experimental commands by Florian Haftmann. The use of Output is
accidental: since these are old-fashioned commands typed into the source
buffer, output is displayed as on a TTY.

I've recently had a private discussion with Florian about this  topic.
We both agreed that the proper way is to integrate such a feature into
the State GUI panel, i.e. to continue it towards an interactive
sketchpad for goal-oriented proof development. When this happens, the
Output panel will be de-emphasized one step further (because it will
stay unchanged and not follow this trend).


	Makarius




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