Re: [isabelle] New error messages in Isabelle 2013



> 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" ...).


I think this point is fundamental with respect to the discussion of the
elimination
of the output window in the near future.

 Apply proof scripts are essential for proof exploration and also as
mentioned
by René above, to the (experimental) understanding of Isabelle automation
proof
procedures as well .

 Would it be possible to do that without the output window?

Best!
On Wed, Jan 30, 2013 at 1:36 PM, René Neumann <rene.neumann at in.tum.de>wrote:

> 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
> better.
>
> TL;DR: Prove one proposition ("have"): old model; overall approach: new
> model.
>
> > 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
>
>


-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil




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