Hi Dmitriy,
If you update to changeset 89b118c0c070, the issue should be resolved.
Lukas
On 10/16/2012 01:41 PM, Dmitriy Traytel wrote:
Hi all,
the following produces a "Loose bound variable" with
Isabelle/4a15873c4ec9
theory Scratch
imports Main
begin
lemma "finite {y |y. ∃x. y ∈ f x}"
apply simp
oops
end
Fortunately, jedit treats a proof that used to work (but fails now due
to the above) as a sorry, such that I can continue working on whatever
follows in the theory until this issue is fixed.
Best wishes,
Dmitriy
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
