src/Sequents/Modal0.ML
author wenzelm
Sun Sep 18 15:20:08 2005 +0200 (2005-09-18)
changeset 17481 75166ebb619b
parent 2073 fb0655539d05
permissions -rw-r--r--
converted to Isar theory format;
     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 = [strimp_def,streqv_def];
    11 
    12 local
    13   val iffR = prove_goal (the_context ())
    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 (the_context ())
    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;