# HG changeset patch
# User clasohm
# Date 826802467 -3600
# Node ID b58a6182e18455a5df85dff918683aa4a9d7405a
# Parent  a84cc626ea6929e480945a4b0c7145e78aa1c8e1
updated syntax of datatype definitions: "C t1 ... tn" instead of "C(t1,...,tn)"

diff -r a84cc626ea69 -r b58a6182e184 doc-src/Logics/HOL.tex
--- a/doc-src/Logics/HOL.tex	Thu Mar 14 12:19:49 1996 +0100
+++ b/doc-src/Logics/HOL.tex	Thu Mar 14 12:21:07 1996 +0100
@@ -1488,7 +1488,7 @@
 \begin{rail}
 typedecl : typevarlist id '=' (cons + '|')
          ;
-cons     : (id | string) ( () | '(' (typ + ',') ')' ) ( () | mixfix )
+cons     : (id | string) (typ *) ( () | mixfix )
          ;
 typ      : typevarlist id
            | tid