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

Lawrence Paulson lp15 at cam.ac.uk
Fri Aug 19 09:27:13 CEST 2011

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

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.

More information about the isabelle-dev mailing list