src/Sequents/Modal0.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 2073 fb0655539d05
child 17481 75166ebb619b
permissions -rw-r--r--
tidying
     1 (*  Title:      Modal/modal0
     2     ID:         $Id$
     3     Author:     Martin Coen
     4     Copyright   1991  University of Cambridge
     5 *)
     6 
     7 structure Modal0_rls = 
     8 struct
     9 
    10 val rewrite_rls = [Modal0.strimp_def,Modal0.streqv_def];
    11 
    12 local
    13   val iffR = prove_goal thy 
    14       "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
    15    (fn prems=>
    16     [ (rewtac iff_def),
    17       (REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]);
    18 
    19   val iffL = prove_goal thy 
    20      "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
    21    (fn prems=>
    22     [ rewtac iff_def,
    23       (REPEAT (resolve_tac (prems@[conjL,impL,basic]) 1)) ])
    24 in
    25 val safe_rls   = [basic,conjL,conjR,disjL,disjR,impL,impR,notL,notR,iffL,iffR];
    26 val unsafe_rls = [allR,exL];
    27 val bound_rls  = [allL,exR];
    28 end
    29 
    30 end;