Re: [isabelle] Isabelle release candidate

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 Isabelle/jEdit.


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