Re: [isabelle] Isabelle release candidate
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
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 Isabelle/jEdit.
This archive was generated by a fusion of
Pipermail (Mailman edition) and