changeset 756 | e0e5c1581e4c |
parent 745 | 45a789407806 |
child 784 | b5adfdad0663 |
--- a/src/FOL/simpdata.ML Wed Nov 30 13:13:52 1994 +0100 +++ b/src/FOL/simpdata.ML Wed Nov 30 13:18:42 1994 +0100 @@ -124,9 +124,8 @@ (*** case splitting ***) -val meta_iffD = - prove_goal FOL.thy "[| P==Q; Q |] ==> P" - (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]) +qed_goal "meta_iffD" FOL.thy "[| P==Q; Q |] ==> P" + (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]); fun split_tac splits = mk_case_split_tac meta_iffD (map mk_meta_eq splits);