updated syntax of primrec definitions
Fri, 12 Jul 1996 17:53:15 +0200
changeset 1854 563dd2b25e37
parent 1853 c18ccd5631e0
child 1855 df6097d0ff2e
updated syntax of primrec definitions
--- 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.
 A theory file may contain any number of {\tt primrec} sections which may be
 intermixed with other declarations.