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)
   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





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