1.1 --- a/doc-src/Ref/theories.tex	Thu Apr 04 18:01:26 1996 +0200
     1.2 +++ b/doc-src/Ref/theories.tex	Thu Apr 04 18:01:47 1996 +0200
     1.3 @@ -112,11 +112,18 @@
     1.4    parse rules ({\tt =>}), print rules ({\tt <=}), and parse/print rules ({\tt
     1.5    ==}).
     1.6  
     1.7 -\item[$rule$]
     1.8 +\item[$rules$]
     1.9    is a series of rule declarations.  Each has a name $id$ and the formula is
    1.10    given by the $string$.  Rule names must be distinct within any single
    1.11    theory file.
    1.12  
    1.13 +\item[$defs$]
    1.14 +  is a series of definitions.  Just like $rules$, except that every $string$
    1.15 +  must be a definition.
    1.16 +
    1.17 +\item[$constdefs$] combines the declaration of constants and their
    1.18 +  definition. The first $string$ is the type, the second the definition.
    1.19 +
    1.20  \item[$ml$] \index{*ML section}
    1.21    consists of \ML\ code, typically for parse and print translation functions.
    1.22  \end{description}

     2.1 --- a/doc-src/Ref/theory-syntax.tex	Thu Apr 04 18:01:26 1996 +0200
     2.2 +++ b/doc-src/Ref/theory-syntax.tex	Thu Apr 04 18:01:47 1996 +0200
     2.3 @@ -32,6 +32,7 @@
     2.4          | types
     2.5          | arities
     2.6          | consts
     2.7 +        | constdefs
     2.8          | trans
     2.9          | defs
    2.10          | rules
    2.11 @@ -85,6 +86,9 @@
    2.12         | infix
    2.13         | 'binder' string nat ;
    2.14  
    2.15 +constdefs : 'constdefs' (id '::' (string | type) string +)
    2.16 +          ;
    2.17 +
    2.18  trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + )
    2.19        ;
    2.20