src/Sequents/Modal0.ML
changeset 17481 75166ebb619b
parent 2073 fb0655539d05
     1.1 --- a/src/Sequents/Modal0.ML	Sun Sep 18 14:25:48 2005 +0200
     1.2 +++ b/src/Sequents/Modal0.ML	Sun Sep 18 15:20:08 2005 +0200
     1.3 @@ -4,19 +4,19 @@
     1.4      Copyright   1991  University of Cambridge
     1.5  *)
     1.6  
     1.7 -structure Modal0_rls = 
     1.8 +structure Modal0_rls =
     1.9  struct
    1.10  
    1.11 -val rewrite_rls = [Modal0.strimp_def,Modal0.streqv_def];
    1.12 +val rewrite_rls = [strimp_def,streqv_def];
    1.13  
    1.14  local
    1.15 -  val iffR = prove_goal thy 
    1.16 +  val iffR = prove_goal (the_context ())
    1.17        "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
    1.18     (fn prems=>
    1.19      [ (rewtac iff_def),
    1.20        (REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]);
    1.21  
    1.22 -  val iffL = prove_goal thy 
    1.23 +  val iffL = prove_goal (the_context ())
    1.24       "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
    1.25     (fn prems=>
    1.26      [ rewtac iff_def,