[isabelle-dev] Summary: WHY have 'a set back?

[Lawrence Paulson]

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?

Larry

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.