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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
