[isabelle-dev] "set_comprehension_pointfree" simproc losing bounds

[Lukas Bulwahn]

Hi Dmitriy,

thanks for the report. I am working on this procedure currently, so this 
will be fixed in a few changesets.

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>