updated syntax of datatype declaration
authorclasohm
Fri, 15 Mar 1996 13:34:39 +0100
changeset 1581 a82618a900e5
parent 1580 e3fd931e6095
child 1582 97a305db0c9e
updated syntax of datatype declaration
doc-src/Logics/HOL.tex
--- a/doc-src/Logics/HOL.tex	Fri Mar 15 12:01:19 1996 +0100
+++ b/doc-src/Logics/HOL.tex	Fri Mar 15 13:34:39 1996 +0100
@@ -1488,12 +1488,9 @@
 \begin{rail}
 typedecl : typevarlist id '=' (cons + '|')
          ;
-cons     : (id | string) (typ *) ( () | mixfix )
+cons     : name (typ *) ( () | mixfix )
          ;
-typ      : typevarlist id
-           | tid
-         ;
-typevarlist : () | tid | '(' (tid + ',') ')'
+typ      : id | tid | ('(' typevarlist id ')')
          ;
 \end{rail}
 \caption{Syntax of datatype declarations}