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

[Jasmin Christian Blanchette]

Hi Florian,

Am 18.08.2011 um 09:18 schrieb Florian Haftmann:

> @list: btw. what is the status of »refute« in general?  Is it supposed
> to be superseded by nitpick entirely?

Pretty much so, yes, but there are a few reasons why I would rather that we keep it around:

1. Refute participates at CASC, where it performs very well. Without Refute, we'd have only two systems (including Satallax) in the higher-order model finding division and there would be no competition.

2. On several occasions Refute has founds models that escaped Nitpick, usually pointing at bugs in Nitpick.

The maintenance load is extremely low. When it comes to the "REFUTE" exception, I can look at it if and when we decide to move back to sets.

Jasmin