[isabelle-dev] list_to_set_comprehension

[Lukas Bulwahn]

On 01/11/2011 05:42 PM, Makarius wrote:
> Changes for list_to_set_comprehension keep coming in, and it seems to 
> be not quite stabilized yet.
>
> Where is the NEWS entry that tells users what to do in case of failure?
>

Here is the NEWS:

* New simproc that rewrites list comprehensions applied to List.set
to set comprehensions.
To deactivate the simproc for historic proof scripts, use:

   [[simproc del: list_to_set_comprehension]]

> Yesterday I have tried to sanitize AFP/JinjaThreads in other repsects, 
> but it did not work (the approximative versions are 
> Isabelle/2aec4b8cd289 AFP/6ac7d314792d).
>
I have worked on Jinja and committed this morning (60003ac7ecd5: fixing 
Jinja theory due to new list_to_set_comprehension simproc).
I fail to build the JinjaThreads image on my local machine, but I do 
follow the AFP status reports.

Lukas
>
>     Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>