src/HOL/Tools/Metis/metis_tactic.ML
changeset 47045 631adf003bb0
parent 47039 1b36a05a070d
child 47047 10bece4ac87e
equal deleted inserted replaced
47044:1ab41ea5b1c6 47045:631adf003bb0
    30 open Metis_Reconstruct
    30 open Metis_Reconstruct
    31 
    31 
    32 val new_skolemizer =
    32 val new_skolemizer =
    33   Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
    33   Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
    34 val advisory_simp =
    34 val advisory_simp =
    35   Attrib.setup_config_bool @{binding metis_advisory_simp} (K false)
    35   Attrib.setup_config_bool @{binding metis_advisory_simp} (K true)
    36 
    36 
    37 (* Designed to work also with monomorphic instances of polymorphic theorems. *)
    37 (* Designed to work also with monomorphic instances of polymorphic theorems. *)
    38 fun have_common_thm ths1 ths2 =
    38 fun have_common_thm ths1 ths2 =
    39   exists (member (Term.aconv_untyped o pairself prop_of) ths1)
    39   exists (member (Term.aconv_untyped o pairself prop_of) ths1)
    40          (map Meson.make_meta_clause ths2)
    40          (map Meson.make_meta_clause ths2)