--- a/doc-src/Ref/theories.tex Thu Apr 04 18:01:26 1996 +0200
+++ b/doc-src/Ref/theories.tex Thu Apr 04 18:01:47 1996 +0200
@@ -112,11 +112,18 @@
parse rules ({\tt =>}), print rules ({\tt <=}), and parse/print rules ({\tt
==}).
-\item[$rule$]
+\item[$rules$]
is a series of rule declarations. Each has a name $id$ and the formula is
given by the $string$. Rule names must be distinct within any single
theory file.
+\item[$defs$]
+ is a series of definitions. Just like $rules$, except that every $string$
+ must be a definition.
+
+\item[$constdefs$] combines the declaration of constants and their
+ definition. The first $string$ is the type, the second the definition.
+
\item[$ml$] \index{*ML section}
consists of \ML\ code, typically for parse and print translation functions.
\end{description}
--- a/doc-src/Ref/theory-syntax.tex Thu Apr 04 18:01:26 1996 +0200
+++ b/doc-src/Ref/theory-syntax.tex Thu Apr 04 18:01:47 1996 +0200
@@ -32,6 +32,7 @@
| types
| arities
| consts
+ | constdefs
| trans
| defs
| rules
@@ -85,6 +86,9 @@
| infix
| 'binder' string nat ;
+constdefs : 'constdefs' (id '::' (string | type) string +)
+ ;
+
trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + )
;