src/FOL/simpdata.ML
changeset 942 d9edeb96b51c
parent 784 b5adfdad0663
child 981 864370666a24
equal deleted inserted replaced
941:f8a202891ac9 942:d9edeb96b51c
   128 (*** case splitting ***)
   128 (*** case splitting ***)
   129 
   129 
   130 qed_goal "meta_iffD" FOL.thy "[| P==Q; Q |] ==> P"
   130 qed_goal "meta_iffD" FOL.thy "[| P==Q; Q |] ==> P"
   131         (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]);
   131         (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]);
   132 
   132 
   133 fun split_tac splits =
   133 local val mktac = mk_case_split_tac meta_iffD
   134     mk_case_split_tac meta_iffD (map mk_meta_eq splits);
   134 in
       
   135 fun split_tac splits = mktac (map mk_meta_eq splits)
       
   136 end;