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
