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
http://isabelle.in.tum.de/repos/isabelle/annotate/9979d64b8016/src/HOL/Product_Type.thy#l1127
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.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
