# 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
    ;