doc-src/Logics/HOL.tex
changeset 1859 2ea3f7ebeccb
parent 1854 563dd2b25e37
child 2495 82ec47e0a8d3
     1.1 --- a/doc-src/Logics/HOL.tex	Fri Jul 12 20:46:32 1996 +0200
     1.2 +++ b/doc-src/Logics/HOL.tex	Mon Jul 15 10:41:30 1996 +0200
     1.3 @@ -1678,7 +1678,7 @@
     1.4    left-hand side, and all recursive calls in $r$ are of the form
     1.5    $f~\dots~y_i~\dots$ for some $i$. There must be exactly one reduction
     1.6    rule for each constructor. Since these reduction rules are mainly used via
     1.7 -  the implicit simpset, their identifiers may also be omitted.
     1.8 +  the implicit simpset, their names may be omitted.
     1.9  \end{itemize}
    1.10  A theory file may contain any number of {\tt primrec} sections which may be
    1.11  intermixed with other declarations.