Re: [isabelle] Isabelle release candidate

Just for the record: In ancient PG, I cannot undo oops in a notepad proof context even if there is no end.


On 28.09.2011 22:12, Makarius wrote:
On Wed, 28 Sep 2011, Andreas Lochbihler wrote:

notepad begin
fix xs ys :: "'a list"
have "xs = ys"
proof(induction xs=="xs" rule: list.induct)

2. Undoing a proof over an oops in a notepad context (as above) does not work
(at least with PG and XEmacs; I haven't tested the other interfaces).

There is a misunderstanding here, and I was first confused myself due to the
unusual indentation style of the above. When you 'oops' out of a proof body,
including notepad, the extra 'end' is already outside of it. So it will normally
close the current theory or locale target or similar.

Here is a working example:

fix x y z
have xxx

lemma "x = x" ..

I did not try it with ancient PG, though, only with current PG 4.1 and


Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft

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