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

[Lawrence Paulson]

It's clear that for inductive definitions, relations are frequently more natural than sets. But I wonder whether a less drastic solution could have been found than abandoning sets altogether. (I'm trying to imagine some sort of magic operator to ease the transition between sets with various forms of tupling and relations.) I certainly find the new world confusing. And of course every set has a function type, which has implications for all the theorem proving tools.
Larry

On 12 Aug 2011, at 10:26, Alexander Krauss wrote:

> In 2007, Stefan reengineered the inductive package, which could only
> define inductive sets at the time. For many applications, inductive
> predicates were more natural, in particular since one could directly
> attach mixfix notation to them, without having to introduce another
> abbreviation. This was a big improvement.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110812/83dd058a/attachment-0002.html>