src/Sequents/Sequents.thy
changeset 14765 bafb24c150c1
parent 7166 a4a870ec2e67
child 14854 61bdf2ae4dc5
     1.1 --- a/src/Sequents/Sequents.thy	Wed May 19 11:41:58 2004 +0200
     1.2 +++ b/src/Sequents/Sequents.thy	Fri May 21 21:14:18 2004 +0200
     1.3 @@ -30,7 +30,7 @@
     1.4  
     1.5  (* concrete syntax *)
     1.6  
     1.7 -types
     1.8 +nonterminals
     1.9    seq seqobj seqcont
    1.10  
    1.11  
    1.12 @@ -59,7 +59,7 @@
    1.13   sequence_name = seq'=>seq'
    1.14  
    1.15  
    1.16 -consts
    1.17 +syntax
    1.18    (*Constant to allow definitions of SEQUENCES of formulas*)
    1.19    "@Side"        :: seq=>(seq'=>seq')     ("<<(_)>>")
    1.20