Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
corrected diagrams for type and simpleType
authorclasohm
Fri, 01 Dec 1995 13:41:48 +0100
changeset 1382 7e97232c1159
parent 1381 57777949b2f8
child 1383 be42217b0b5c
corrected diagrams for type and simpleType
doc-src/Ref/theory-syntax.tex file | annotate | diff | comparison | revisions 
--- a/doc-src/Ref/theory-syntax.tex	Fri Dec 01 13:03:34 1995 +0100
+++ b/doc-src/Ref/theory-syntax.tex	Fri Dec 01 13:41:48 1995 +0100
@@ -70,13 +70,13 @@
 consts : 'consts' ( ( constDecl ( () | ( '(' mixfix ')' ) ) ) + )
        ;
 
-constDecl : ( name + ',') '::' (string | constType);
+constDecl : ( name + ',') '::' (string | type);
 
-constType : simpleType | '(' constType ')' | '[' ( constType + "," ) ']'
-            '=>' constType | constType '=>' constType;
+type : simpleType | '(' type ')' | type '=>' type |
+       '[' ( type + "," ) ']' '=>' type;
 
 simpleType: id | ( tid ( () | '::' id ) ) |
-            '(' ( constType + "," ) ')' ( id + ',' ) | simpleType ( id + ',' );
+            '(' ( type + "," ) ')' id | simpleType id;
 
 mixfix :  string ( () | ( () | ('[' (nat + ',') ']')) nat )
        | infix
isabelle