# HG changeset patch
# User nipkow
# Date 828633707 -7200
# Node ID a4ed2655b08ccdbd0d22347bb00145b1f8f614af
# Parent  c4901f7161c587ff570d581e91a9160564a1ea3c
Added 'constdefs'

diff -r c4901f7161c5 -r a4ed2655b08c doc-src/Ref/theories.tex
--- 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}
diff -r c4901f7161c5 -r a4ed2655b08c doc-src/Ref/theory-syntax.tex
--- 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 + )
       ;