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

[Jasmin Christian Blanchette]

Am 18.08.2011 um 21:40 schrieb Alexander Krauss:

> On 08/18/2011 02:16 PM, Florian Haftmann wrote:
>> * (maybe)
>>   >  hide_fact (open) Set.mem_def Set.Collect_def
>>   to indicate that something is going on with these
> 
> maybe also declare them [no_atp], to avoid sledgehammer-generated proofs that we know are going to break one release later...?

Sounds like a good idea, but make sure also to remove the following lines in "sledgehammer_filter.ML":

(* Set constants tend to pull in too many irrelevant facts. We limit the damage
   by treating them more or less as if they were built-in but add their
   definition at the end. *)
val set_consts =
  [(@{const_name Collect}, @{thms Collect_def}),
   (@{const_name Set.member}, @{thms mem_def})]

And (effectively) replace "set_consts" with the empty list, ideally simplifying the code as you go. This will degrade the quality of the relevance filtering slightly, but would have to be done anyway when "'a set" is reintroduced.

Jasmin