Re: [isabelle] Isabelle release candidate



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

Andreas

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)
print_cases
oops
end

2. Undoing a proof over an oops in a notepad context (as above) does not work
(at least with PG 3.7.1.1. 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:

notepad
begin
fix x y z
have xxx
oops

lemma "x = x" ..

I did not try it with ancient PG 3.7.1.1, though, only with current PG 4.1 and
Isabelle/jEdit.


Makarius

--
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.edu
http://pp.info.uni-karlsruhe.de
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.