src/Sequents/Sequents.thy
changeset 14765 bafb24c150c1
parent 7166 a4a870ec2e67
child 14854 61bdf2ae4dc5
--- a/src/Sequents/Sequents.thy	Wed May 19 11:41:58 2004 +0200
+++ b/src/Sequents/Sequents.thy	Fri May 21 21:14:18 2004 +0200
@@ -30,7 +30,7 @@
 
 (* concrete syntax *)
 
-types
+nonterminals
   seq seqobj seqcont
 
 
@@ -59,7 +59,7 @@
  sequence_name = seq'=>seq'
 
 
-consts
+syntax
   (*Constant to allow definitions of SEQUENCES of formulas*)
   "@Side"        :: seq=>(seq'=>seq')     ("<<(_)>>")