src/Tools/coherent.ML
changeset 36945 9bec62c10714
parent 32740 9dd0a2f83429
child 36946 4eba866311df
equal deleted inserted replaced
36944:dbf831a50e4a 36945:9bec62c10714
    44 local open Conv in
    44 local open Conv in
    45 
    45 
    46 fun rulify_elim_conv ct =
    46 fun rulify_elim_conv ct =
    47   if is_atomic (Logic.strip_imp_concl (term_of ct)) then all_conv ct
    47   if is_atomic (Logic.strip_imp_concl (term_of ct)) then all_conv ct
    48   else concl_conv (length (Logic.strip_imp_prems (term_of ct)))
    48   else concl_conv (length (Logic.strip_imp_prems (term_of ct)))
    49     (rewr_conv (symmetric Data.atomize_elimL) then_conv
    49     (rewr_conv (Thm.symmetric Data.atomize_elimL) then_conv
    50      MetaSimplifier.rewrite true (map symmetric
    50      MetaSimplifier.rewrite true (map Thm.symmetric
    51        [Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct
    51        [Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct
    52 
    52 
    53 end;
    53 end;
    54 
    54 
    55 fun rulify_elim th = Simplifier.norm_hhf (Conv.fconv_rule rulify_elim_conv th);
    55 fun rulify_elim th = Simplifier.norm_hhf (Conv.fconv_rule rulify_elim_conv th);