--- a/doc-src/Ref/theory-syntax.tex Fri Dec 01 14:17:50 1995 +0100
+++ b/doc-src/Ref/theory-syntax.tex Fri Dec 01 14:20:09 1995 +0100
@@ -53,7 +53,14 @@
types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + )
;
-typeDecl : ( () | tid | '(' ( tid + ',' ) ')') name ( () | '=' string );
+typeDecl : ( () | tid | '(' ( tid + ',' ) ')') name
+ ( () | '=' ( string | type ) );
+
+type : simpleType | '(' type ')' | type '=>' type |
+ '[' ( type + "," ) ']' '=>' type;
+
+simpleType: id | ( tid ( () | '::' id ) ) |
+ '(' ( type + "," ) ')' id | simpleType id;
infix : ( 'infixr' | 'infixl' ) nat;
@@ -72,12 +79,6 @@
constDecl : ( name + ',') '::' (string | type);
-type : simpleType | '(' type ')' | type '=>' type |
- '[' ( type + "," ) ']' '=>' type;
-
-simpleType: id | ( tid ( () | '::' id ) ) |
- '(' ( type + "," ) ')' id | simpleType id;
-
mixfix : string ( () | ( () | ('[' (nat + ',') ']')) nat )
| infix
| 'binder' string nat ;