Re: [isabelle] Isabelle release candidate
Just for the record: In ancient PG 126.96.36.199, 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:
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 188.8.131.52. 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
lemma "x = x" ..
I did not try it with ancient PG 184.108.40.206, though, only with current PG 4.1 and
Karlsruher Institut für Technologie
Adenauerring 20a, Geb. 50.41, Raum 031
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
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