--- a/doc-src/Ref/theory-syntax.tex Wed Nov 29 16:56:54 1995 +0100
+++ b/doc-src/Ref/theory-syntax.tex Wed Nov 29 16:58:30 1995 +0100
@@ -70,8 +70,23 @@
consts : 'consts' ( ( constDecl ( () | ( '(' mixfix ')' ) ) ) + )
;
-constDecl : ( name + ',') '::' string ;
+constDecl : ( name + ',') '::' (string | constType) ;
+
+constType : ( applParam * ) applLast;
+
+applParam : ( complexType | '(' paramType ')' |
+ '[' (paramType + ',') ']' ) '=>';
+
+applLast: ( simpleType | '(' (paramType + ',') ')' ) (id *);
+complexType: ( simpleType | '(' complexType ')' ) ( id + ) |
+ '(' ( ( complexType | '(' complexType ')' ) + ',' ) ')'
+ id +;
+
+paramType: ( complexType | '(' paramType ')' | '[' ( paramType + ',' ) ']' )
+ ( '=>' paramType * );
+
+simpleType: id | ( tid ( () | '::' id ) );
mixfix : string ( () | ( () | ('[' (nat + ',') ']')) nat )
| infix