# HG changeset patch # User nipkow # Date 799437546 -7200 # Node ID 13c35eb5169ba6d2ab079474d74f5faa248203b8 # Parent 2f9f2ea26f8fa48c53737bc843a65addefd045f5 Sections can now be given in any order. diff -r 2f9f2ea26f8f -r 13c35eb5169b doc-src/Ref/theory-syntax.tex --- a/doc-src/Ref/theory-syntax.tex Mon May 01 11:17:41 1995 +0200 +++ b/doc-src/Ref/theory-syntax.tex Tue May 02 19:59:06 1995 +0200 @@ -25,26 +25,32 @@ name: id | string; -extension : classes default types arities consts trans rules \\ 'end' ml - ; +extension : (section +) 'end' ml; -classes : () - | 'classes' ( ( id ( () +section : classes + | default + | types + | arities + | consts + | trans + | defs + | rules + ; + +classes : 'classes' ( ( id ( () | '<' (id + ',') ) ) + ) ; -default : () - | 'default' sort +default : 'default' sort ; sort : id | '\{' (id * ',') '\}' ; -types : () - | 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + ) +types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + ) ; typeDecl : ( () | tid | '(' ( tid + ',' ) ')') name ( () | '=' string ); @@ -52,8 +58,7 @@ infix : ( 'infixr' | 'infixl' ) nat; -arities : () - | 'arities' ((( name + ',' ) '::' arity ) + ) +arities : 'arities' ((( name + ',' ) '::' arity ) + ) ; arity : ( () @@ -62,8 +67,7 @@ ; -consts : () - | 'consts' ( ( constDecl ( () | ( '(' mixfix ')' ) ) ) + ) +consts : 'consts' ( ( constDecl ( () | ( '(' mixfix ')' ) ) ) + ) ; constDecl : ( name + ',') '::' string ; @@ -73,16 +77,17 @@ | infix | 'binder' string nat ; -trans : () - | 'translations' ( pat ( '==' | '=>' | '<=' ) pat + ) +trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + ) ; pat : ( () | ( '(' id ')' ) ) string; -rules : () - | 'rules' (( id string ) + ) +rules : 'rules' (( id string ) + ) ; +defs : 'defs' (( id string ) + ) + ; + ml : () | 'ML' text ;