added "Collect_cong" to cover extensionality of "Collect" (special cases of "ext" pass through the relevant filter)
authorblanchet
Thu May 17 13:36:23 2012 +0200 (2012-05-17)
changeset 479399ff976a6c2cb
parent 47938 2924f37cb6b3
child 47940 4ef90b51641e
added "Collect_cong" to cover extensionality of "Collect" (special cases of "ext" pass through the relevant filter)
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed May 16 19:20:19 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu May 17 13:36:23 2012 +0200
     1.3 @@ -366,7 +366,7 @@
     1.4     by treating them more or less as if they were built-in but add their
     1.5     axiomatization at the end. *)
     1.6  val set_consts = [@{const_name Collect}, @{const_name Set.member}]
     1.7 -val set_thms = @{thms Collect_mem_eq mem_Collect_eq}
     1.8 +val set_thms = @{thms Collect_mem_eq mem_Collect_eq Collect_cong}
     1.9  
    1.10  fun add_pconsts_in_term thy is_built_in_const also_skolems pos =
    1.11    let
    1.12 @@ -777,6 +777,7 @@
    1.13                      |> chop special_fact_index
    1.14          in bef @ add @ after end
    1.15      fun insert_special_facts accepts =
    1.16 +       (* FIXME: get rid of "ext" here once it is treated as a helper *)
    1.17         [] |> could_benefit_from_ext is_built_in_const accepts ? cons @{thm ext}
    1.18            |> add_set_const_thms accepts
    1.19            |> insert_into_facts accepts