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

[Alexander Krauss]

On 08/12/2011 02:16 PM, Tobias Nipkow wrote:
> Surely we want to maintain both inductive and inductive_set?

This is what Florian's experiment does. It basically reverts the 2008 
transition, but not the 2007 one.

Alex