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

[Jasmin Christian Blanchette]

Am 18.08.2011 um 09:18 schrieb Florian Haftmann:

> Strange.  I guess refute was not modified in 2008 (at least according to
> hg diff -r e8cc166ba123 -r ec46381f149d | grep -i refute).  Maybe this
> crept in silently over the last years?

It was not modified in 2008, but it was modified in 2009. It wasn't using antiquotation, so its support for "set"s was just hanging around dead. If you look more closely at the history, you'll see what needs to be reverted.

Jasmin