src/FOL/ex/If.ML

--- a/src/FOL/ex/If.ML	Mon Nov 21 14:06:59 1994 +0100
+++ b/src/FOL/ex/If.ML	Mon Nov 21 14:11:21 1994 +0100
@@ -12,13 +12,13 @@
 val prems = goalw If.thy [if_def]
     "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)";
 by (fast_tac (FOL_cs addIs prems) 1);
-val ifI = result();
+qed "ifI";
 
 val major::prems = goalw If.thy [if_def]
    "[| if(P,Q,R);  [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S";
 by (cut_facts_tac [major] 1);
 by (fast_tac (FOL_cs addIs prems) 1);
-val ifE = result();
+qed "ifE";
 
 
 goal If.thy