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

Lawrence Paulson lp15 at cam.ac.uk
Fri Aug 12 13:01:00 CEST 2011

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.

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>

More information about the isabelle-dev mailing list