src/Sequents/Sequents.thy
author paulson
Mon, 06 Aug 2001 12:42:43 +0200
changeset 11461 ffeac9aa1967
parent 7166 a4a870ec2e67
child 14765 bafb24c150c1
permissions -rw-r--r--
removed an unsuitable default simprule
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6819
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
     1
(*  Title: 	Sequents/Sequents.thy
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     2
    ID:         $Id$
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     5
7166
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
     6
Basis theory for parsing and pretty-printing of sequences to be used in
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
     7
Sequent Calculi. 
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     8
*)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
     9
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    10
Sequents = Pure +
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    11
7098
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents: 6819
diff changeset
    12
global
86583034aacf installation of simplifier and classical reasoner, better rules etc
paulson
parents: 6819
diff changeset
    13
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    14
types
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    15
  o 
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    16
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    17
arities
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    18
  o :: logic
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    19
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    20
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    21
(* Sequences *)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    22
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    23
types
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    24
 seq'
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    25
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    26
consts
7166
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
    27
 SeqO'         :: [o,seq']=>seq'
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
    28
 Seq1'         :: o=>seq'
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    29
    
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    30
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    31
(* concrete syntax *)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    32
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    33
types
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    34
  seq seqobj seqcont
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    35
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    36
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    37
syntax
7166
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
    38
 SeqEmp         :: seq                                ("")
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
    39
 SeqApp         :: [seqobj,seqcont] => seq            ("__")
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    40
7166
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
    41
 SeqContEmp     :: seqcont                            ("")
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
    42
 SeqContApp     :: [seqobj,seqcont] => seqcont        (",/ __")
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    43
  
7166
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
    44
 SeqO           :: o => seqobj                        ("_")
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
    45
 SeqId          :: 'a => seqobj                       ("$_")
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    46
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    47
types
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    48
    
7166
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
    49
 single_seqe = [seq,seqobj] => prop
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
    50
 single_seqi = [seq'=>seq',seq'=>seq'] => prop
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
    51
 two_seqi    = [seq'=>seq', seq'=>seq'] => prop
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
    52
 two_seqe    = [seq, seq] => prop
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
    53
 three_seqi  = [seq'=>seq', seq'=>seq', seq'=>seq'] => prop
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
    54
 three_seqe  = [seq, seq, seq] => prop
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
    55
 four_seqi   = [seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
    56
 four_seqe   = [seq, seq, seq, seq] => prop
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
    57
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
    58
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
    59
 sequence_name = seq'=>seq'
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
    60
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
    61
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
    62
consts
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
    63
  (*Constant to allow definitions of SEQUENCES of formulas*)
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
    64
  "@Side"        :: seq=>(seq'=>seq')     ("<<(_)>>")
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    65
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    66
end
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    67
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    68
ML
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    69
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    70
(* parse translation for sequences *)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    71
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    72
fun abs_seq' t = Abs("s", Type("seq'",[]), t);
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    73
6819
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
    74
fun seqobj_tr(Const("SeqO",_) $ f) = Const("SeqO'",dummyT) $ f |
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
    75
    seqobj_tr(_ $ i) = i;
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    76
    
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    77
fun seqcont_tr(Const("SeqContEmp",_)) = Bound 0 |
6819
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
    78
    seqcont_tr(Const("SeqContApp",_) $ so $ sc) = 
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
    79
      (seqobj_tr so) $ (seqcont_tr sc);
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    80
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    81
fun seq_tr(Const("SeqEmp",_)) = abs_seq'(Bound 0) |
6819
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
    82
    seq_tr(Const("SeqApp",_) $ so $ sc) = 
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
    83
      abs_seq'(seqobj_tr(so) $ seqcont_tr(sc));
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    84
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    85
6819
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
    86
fun singlobj_tr(Const("SeqO",_) $ f) =
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
    87
    abs_seq' ((Const("SeqO'",dummyT) $ f) $ Bound 0);
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    88
    
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    89
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    90
    
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    91
(* print translation for sequences *)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    92
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    93
fun seqcont_tr' (Bound 0) = 
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    94
      Const("SeqContEmp",dummyT) |
6819
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
    95
    seqcont_tr' (Const("SeqO'",_) $ f $ s) =
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
    96
      Const("SeqContApp",dummyT) $ 
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
    97
      (Const("SeqO",dummyT) $ f) $ 
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    98
      (seqcont_tr' s) |
6819
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
    99
(*    seqcont_tr' ((a as Abs(_,_,_)) $ s)= 
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   100
      seqcont_tr'(betapply(a,s)) | *)
6819
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
   101
    seqcont_tr' (i $ s) = 
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
   102
      Const("SeqContApp",dummyT) $ 
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
   103
      (Const("SeqId",dummyT) $ i) $ 
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   104
      (seqcont_tr' s);
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   105
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   106
fun seq_tr' s =
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   107
    let fun seq_itr' (Bound 0) = 
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   108
              Const("SeqEmp",dummyT) |
6819
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
   109
            seq_itr' (Const("SeqO'",_) $ f $ s) =
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
   110
              Const("SeqApp",dummyT) $ 
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
   111
              (Const("SeqO",dummyT) $ f) $ (seqcont_tr' s) |
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
   112
(*            seq_itr' ((a as Abs(_,_,_)) $ s) =
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   113
              seq_itr'(betapply(a,s)) |    *)
6819
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
   114
            seq_itr' (i $ s) =
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
   115
              Const("SeqApp",dummyT) $ 
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
   116
              (Const("SeqId",dummyT) $ i) $ 
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   117
              (seqcont_tr' s)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   118
    in case s of 
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   119
         Abs(_,_,t) => seq_itr' t |
6819
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
   120
         _ => s $ (Bound 0)
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   121
    end;
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   122
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   123
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   124
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   125
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   126
fun single_tr c [s1,s2] =
6819
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
   127
    Const(c,dummyT) $ seq_tr s1 $ singlobj_tr s2;
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   128
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   129
fun two_seq_tr c [s1,s2] =
6819
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
   130
    Const(c,dummyT) $ seq_tr s1 $ seq_tr s2;
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   131
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   132
fun three_seq_tr c [s1,s2,s3] =
6819
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
   133
    Const(c,dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3;
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   134
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   135
fun four_seq_tr c [s1,s2,s3,s4] =
6819
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
   136
    Const(c,dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4;
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   137
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   138
6819
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
   139
fun singlobj_tr'(Const("SeqO'",_) $ fm) = fm |
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
   140
    singlobj_tr'(id) = Const("@SeqId",dummyT) $ id;
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   141
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   142
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   143
fun single_tr' c [s1, s2] =
6819
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
   144
(Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 ); 
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   145
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   146
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   147
fun two_seq_tr' c [s1, s2] =
6819
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
   148
  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2; 
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   149
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   150
fun three_seq_tr' c [s1, s2, s3] =
6819
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
   151
  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3; 
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   152
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   153
fun four_seq_tr' c [s1, s2, s3, s4] =
6819
433a980103b4 fixed title line; added spacing
paulson
parents: 2073
diff changeset
   154
  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3 $ seq_tr' s4; 
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   155
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   156
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   157
			 
7166
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
   158
(** for the <<...>> notation **)
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
   159
  
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
   160
fun side_tr [s1] = seq_tr s1;
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
   161
a4a870ec2e67 Sara Kalvala: moving the <<...>> notation from LK to Sequents
paulson
parents: 7121
diff changeset
   162
val parse_translation = [("@Side", side_tr)];