# HG changeset patch
# User clasohm
# Date 786197922 -3600
# Node ID e0e5c1581e4c47a289567ed2cbe6622b024546f9
# Parent  dfb3894d78e4fa1744b1e910412d129ce4d575fe
added qed_goal for meta_iffD

diff -r dfb3894d78e4 -r e0e5c1581e4c src/FOL/simpdata.ML
--- 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);