# HG changeset patch
# User paulson
# Date 900583856 -7200
# Node ID 5b63f591678bd7a946eec4edf80222686d8ff8f9
# Parent  1e944fe5ce96e4739014a39adbc739591af2e0e0
tidying

diff -r 1e944fe5ce96 -r 5b63f591678b src/FOL/ex/If.ML
--- a/src/FOL/ex/If.ML	Thu Jul 16 11:50:01 1998 +0200
+++ b/src/FOL/ex/If.ML	Thu Jul 16 12:10:56 1998 +0200
@@ -9,20 +9,19 @@
 open If;
 open Cla;    (*in case structure IntPr is open!*)
 
-val prems = goalw If.thy [if_def]
+val prems = Goalw [if_def]
     "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)";
 by (blast_tac (claset() addIs prems) 1);
 qed "ifI";
 
-val major::prems = goalw If.thy [if_def]
+val major::prems = Goalw [if_def]
    "[| if(P,Q,R);  [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S";
 by (cut_facts_tac [major] 1);
 by (blast_tac (claset() addIs prems) 1);
 qed "ifE";
 
 
-Goal
-    "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
+Goal "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
 by (rtac iffI 1);
 by (etac ifE 1);
 by (etac ifE 1);