# HG changeset patch
# User berghofe
# Date 837186795 -7200
# Node ID 563dd2b25e3757a7b1d0e52daa69e44711456200
# Parent  c18ccd5631e07f4ee1f9e91e0e6fac9a996d6c27
updated syntax of primrec definitions

diff -r c18ccd5631e0 -r 563dd2b25e37 doc-src/Logics/HOL.tex
--- a/doc-src/Logics/HOL.tex	Fri Jul 12 16:52:29 1996 +0200
+++ b/doc-src/Logics/HOL.tex	Fri Jul 12 17:53:15 1996 +0200
@@ -1677,7 +1677,8 @@
   constructor of the datatype, $r$ contains only the free variables on the
   left-hand side, and all recursive calls in $r$ are of the form
   $f~\dots~y_i~\dots$ for some $i$. There must be exactly one reduction
-  rule for each constructor.
+  rule for each constructor. Since these reduction rules are mainly used via
+  the implicit simpset, their identifiers may also be omitted.
 \end{itemize}
 A theory file may contain any number of {\tt primrec} sections which may be
 intermixed with other declarations.