[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

[Lawrence Paulson]

I am currently working on AFP/Coinductive, which is full of the sort of thing.
Larry

On 19 Aug 2011, at 00:31, Gerwin Klein wrote:

> Can't really quantify it, but I'm seeing this all the time from not-so-novice users over here. Mixing sets and predicates (e.g. using intersection on predicates) works often enough that people like it and overuse it. Sooner or later you will see unfolding of mem_def. As opposed to unfolding conjunction, unfolding mem_def proves things that otherwise simp/auto/etc fail on.