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

Lawrence Paulson lp15 at cam.ac.uk
Thu Aug 11 15:09:31 CEST 2011

I hope that my position on this question is obvious. And if we decide to revert to the former setup, I would be happy to help track down and fix some problems in theories.

On 11 Aug 2011, at 13:43, Florian Haftmann wrote:

> Why (I think) the current state concerning sets is a bad idea:
> * There are two worlds (sets and predicates) which are logically the
> same but syntactically different.  Although the logic construction
> suggests that you can switch easily between both, in practice you can't

More information about the isabelle-dev mailing list