[isabelle-dev] "set_comprehension_pointfree" simproc losing bounds

Dmitriy Traytel traytel at in.tum.de
Tue Oct 16 13:41:12 CEST 2012

Hi all,

the following produces a "Loose bound variable" with Isabelle/4a15873c4ec9

theory Scratch
imports Main

lemma "finite {y |y. ∃x. y ∈ f x}"
apply simp


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,

More information about the isabelle-dev mailing list