src/Modal/ROOT.ML

-(*  Title: 	91/Modal/ROOT
+(*  Title:      91/Modal/ROOT
     ID:         $Id$
-    Author: 	Martin Coen
+    Author:     Martin Coen
     Copyright   1991  University of Cambridge
 *)
 
 val banner = "Modal Logic (over LK)";
 writeln banner;

 
 local
   val iffR = prove_goal thy 
       "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
    (fn prems=>
-    [ (rewrite_goals_tac [iff_def]),
+    [ (rewtac iff_def),
       (REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]);
 
   val iffL = prove_goal thy 
      "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
    (fn prems=>
-    [ rewrite_goals_tac [iff_def],
+    [ rewtac iff_def,
       (REPEAT (resolve_tac (prems@[conjL,impL,basic]) 1)) ])
 in
 val safe_rls   = [basic,conjL,conjR,disjL,disjR,impL,impR,notL,notR,iffL,iffR];
 val unsafe_rls = [allR,exL];
 val bound_rls  = [allL,exR];

     val aside_rls   = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2,S43pi0,S43pi1,S43pi2]
    end;
 end;
 structure S43_Prover = Modal_ProverFun(MP_Rule);  
 
-val Modal_build_completed = ();	(*indicate successful build*)
+val Modal_build_completed = (); (*indicate successful build*)
 
 (*printing functions are inherited from LK*)