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

Alexander Krauss krauss at in.tum.de
Fri Aug 12 14:25:06 CEST 2011

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.


More information about the isabelle-dev mailing list