Re: [isabelle] New error messages in Isabelle 2013

Am 30.01.2013 15:47, schrieb Makarius:
> On Wed, 30 Jan 2013, René Neumann wrote:
>> Please keep in mind, that the good ol' TTY approach with only one single
>> point of focus is not overall obsolete: When dealing with a single
>> proof, one normally only focuses on the lines one is writing.
> This is even before Proof General and especially before Isar proofs. Can
> you show some of your proofs that you normally do?

Sorry. Probably we misunderstood each other here. By TTY(-like) approach
I meant the PG-approach of feeding line by line (resp instruction by
instruction) to the prover.

If I want to proof something (especially in apply-style which sometimes
pre-dates an isar-proof to get some inspiration of what the tools are
able to proof automatically), I really like to only feed command by
command to the prover ("what are the goals exactly after the 'with'",
"what does simp remove/unfold", "what goals does 'induction' give" ...).
Of course these points where I'm doing so might be scattered throughout
the theories. So when switching between points, the new model is clearly

TL;DR: Prove one proposition ("have"): old model; overall approach: new

> Or did you mean a keyboard version of "hover over squiggles"?

This I meant by "would also be cumbersome".

René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Kryptografische Unterschrift

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