[isabelle-dev] list_to_set_comprehension

Lukas Bulwahn bulwahn at in.tum.de
Tue Jan 11 17:59:09 CET 2011

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.

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

More information about the isabelle-dev mailing list