# HG changeset patch # User wenzelm # Date 863790844 -7200 # Node ID 9e097d5cc246da4e854e8a3aabd3d71cf1832254 # Parent 409382c0cc881c0f3cd785bf0153ac3eec5e8599 fixed infix syntax; diff -r 409382c0cc88 -r 9e097d5cc246 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 + )