src/Sequents/Modal0.thy
changeset 17481 75166ebb619b
parent 14765 bafb24c150c1
child 21426 87ac12bed1ab
     1.1 --- a/src/Sequents/Modal0.thy	Sun Sep 18 14:25:48 2005 +0200
     1.2 +++ b/src/Sequents/Modal0.thy	Sun Sep 18 15:20:08 2005 +0200
     1.3 @@ -1,42 +1,43 @@
     1.4 -(*  Title:      Sequents/Modal0
     1.5 +(*  Title:      Sequents/Modal0.thy
     1.6      ID:         $Id$
     1.7      Author:     Martin Coen
     1.8      Copyright   1991  University of Cambridge
     1.9  *)
    1.10  
    1.11 -Modal0 = LK0 +
    1.12 +theory Modal0
    1.13 +imports LK0
    1.14 +uses "modal.ML"
    1.15 +begin
    1.16  
    1.17  consts
    1.18    box           :: "o=>o"       ("[]_" [50] 50)
    1.19    dia           :: "o=>o"       ("<>_" [50] 50)
    1.20 -  "--<",">-<"   :: "[o,o]=>o"   (infixr 25)
    1.21 -  Lstar,Rstar   :: "two_seqi"
    1.22 +  "--<"         :: "[o,o]=>o"   (infixr 25)
    1.23 +  ">-<"         :: "[o,o]=>o"   (infixr 25)
    1.24 +  Lstar         :: "two_seqi"
    1.25 +  Rstar         :: "two_seqi"
    1.26  
    1.27  syntax
    1.28    "@Lstar"      :: "two_seqe"   ("(_)|L>(_)" [6,6] 5)
    1.29    "@Rstar"      :: "two_seqe"   ("(_)|R>(_)" [6,6] 5)
    1.30  
    1.31 -rules
    1.32 -  (* Definitions *)
    1.33 -
    1.34 -  strimp_def    "P --< Q == [](P --> Q)"
    1.35 -  streqv_def    "P >-< Q == (P --< Q) & (Q --< P)"
    1.36 -end
    1.37 -
    1.38 -ML
    1.39 -
    1.40 -local
    1.41 -
    1.42 +ML {*
    1.43    val Lstar = "Lstar";
    1.44    val Rstar = "Rstar";
    1.45    val SLstar = "@Lstar";
    1.46    val SRstar = "@Rstar";
    1.47  
    1.48 -  fun star_tr c [s1,s2] =
    1.49 -      Const(c,dummyT)$Sequents.seq_tr s1$Sequents.seq_tr s2;
    1.50 -  fun star_tr' c [s1,s2] = 
    1.51 -      Const(c,dummyT) $ Sequents.seq_tr' s1 $ Sequents.seq_tr' s2;
    1.52 -in
    1.53 -val parse_translation = [(SLstar,star_tr Lstar), (SRstar,star_tr Rstar)];
    1.54 -val print_translation = [(Lstar,star_tr' SLstar), (Rstar,star_tr' SRstar)]
    1.55 -end;
    1.56 +  fun star_tr c [s1,s2] = Const(c,dummyT)$ seq_tr s1$ seq_tr s2;
    1.57 +  fun star_tr' c [s1,s2] = Const(c,dummyT) $ seq_tr' s1 $ seq_tr' s2;
    1.58 +*}
    1.59 +
    1.60 +parse_translation {* [(SLstar,star_tr Lstar), (SRstar,star_tr Rstar)] *}
    1.61 +print_translation {* [(Lstar,star_tr' SLstar), (Rstar,star_tr' SRstar)] *}
    1.62 +
    1.63 +defs
    1.64 +  strimp_def:    "P --< Q == [](P --> Q)"
    1.65 +  streqv_def:    "P >-< Q == (P --< Q) & (Q --< P)"
    1.66 +
    1.67 +ML {* use_legacy_bindings (the_context ()) *}
    1.68 +
    1.69 +end