[isabelle-dev] set_comprehension_pointfree simproc

Makarius makarius at sketis.net
Fri Mar 14 13:36:37 CET 2014

What is the status of the set_comprehension_pointfree simproc?

In 31afce809794 Dmitriy says "set_comprehension_pointfree simproc causes 
to many surprises if enabled by default", and in 4d899933a51a I've tried 
to reconstruct the missing NEWS entry, since this is cleary a 
user-relevant change.

Looking around in the sources and the history, e.g. 9979d64b8016 where 
Lukas Bulwahn is "moving simproc from Finite_Set to more appropriate 
Product_Type theory" shows that there is a related 
Set_Comprehension_Pointfree.code_simproc still present today 

Does anybody understand how the tool was initially intended to work?  Is 
it feasible to move it just in one place?  Lets say 
src/HOL/Library/Set_Comprehension_Pointfree.thy, so that the applications 
that need it can import just that theory, and main HOL remains clear.


More information about the isabelle-dev mailing list