[isabelle-dev] Summary: WHY have 'a set back?
lp15 at cam.ac.uk
Tue Aug 30 22:34:29 CEST 2011
I have converted these two examples, although I'm sure there are others. I certainly agree with your analysis.
As a way of assisting users in the conversion (and warning them of potential incompatibilities), can't we hide the theorems mem_def and Collect_def?
On 30 Aug 2011, at 21:31, Alexander Krauss wrote:
> 2.1. Quite a lot of work for users out there: Cleaning up set/pred
> confusion from our own theories and the AFP is already taking
> significant time. Some newer AFP entries where confusion occurs also
> in definitions and lemmas (in particular DataRefinementIBP and
> GraphMarkingIBP) require significant reengineering. (The original
> author, Viorel Preoteasa kindly agreed to help us here). But even
> for those theories it seems that the changes improve overall
> readability and automation.
More information about the isabelle-dev