fixed infix syntax;
authorwenzelm
Fri, 16 May 1997 15:54:04 +0200
changeset 3215 9e097d5cc246
parent 3214 409382c0cc88
child 3216 fdcb907f9c93
fixed infix syntax;
doc-src/Ref/theory-syntax.tex
--- a/doc-src/Ref/theory-syntax.tex	Fri May 16 15:53:35 1997 +0200
+++ b/doc-src/Ref/theory-syntax.tex	Fri May 16 15:54:04 1997 +0200
@@ -69,7 +69,7 @@
 types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + )
       ;
 
-infix : ( 'infixr' | 'infixl' ) nat
+infix : ( 'infixr' | 'infixl' ) (() | string) nat
       ;
 
 typeDecl : typevarlist name
@@ -104,7 +104,7 @@
 constDecl : ( name + ',') '::' (string | type);
 
 mixfix :  string ( () | ( () | ('[' (nat + ',') ']')) nat )
-       | ( 'infixr' | 'infixl' ) (() | string) nat
+       |  infix
        | 'binder' string nat ;
 
 trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + )