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

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Thu Aug 18 09:35:47 CEST 2011

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.


More information about the isabelle-dev mailing list