equal
deleted
inserted
replaced
75 *) |
75 *) |
76 fun transform_prem ctxt names thm = |
76 fun transform_prem ctxt names thm = |
77 let |
77 let |
78 fun split_conj names (Const ("op &", _) $ f1 $ f2) = |
78 fun split_conj names (Const ("op &", _) $ f1 $ f2) = |
79 (case head_of f1 of |
79 (case head_of f1 of |
80 Const (name, _) => if name mem names then SOME f2 else NONE |
80 Const (name, _) => if member (op =) names name then SOME f2 else NONE |
81 | _ => NONE) |
81 | _ => NONE) |
82 | split_conj _ _ = NONE; |
82 | split_conj _ _ = NONE; |
83 in |
83 in |
84 map_thm ctxt (split_conj names) (etac conjunct2 1) thm |
84 map_thm ctxt (split_conj names) (etac conjunct2 1) thm |
85 end |
85 end |