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

[Tobias Nipkow]

Surely we want to maintain both inductive and inductive_set?

Tobias

Am 12/08/2011 13:01, schrieb 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.
> 
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev