doc-src/IsarRef/hol.tex
changeset 8657 b9475dad85ed
parent 8547 93b8685d004b
child 8665 403c2985e65e
     1.1 --- a/doc-src/IsarRef/hol.tex	Sat Apr 01 20:18:52 2000 +0200
     1.2 +++ b/doc-src/IsarRef/hol.tex	Sat Apr 01 20:21:39 2000 +0200
     1.3 @@ -129,9 +129,14 @@
     1.4  \end{matharray}
     1.5  
     1.6  \begin{rail}
     1.7 -  'primrec' parname? (thmdecl? prop comment? + )
     1.8 +  'primrec' parname? (equation + )
     1.9 +  ;
    1.10 +  'recdef' name term (equation +) hints
    1.11    ;
    1.12 -  'recdef' name term (term comment? +) \\ ('congs' thmrefs)? ('simpset' name)?
    1.13 +
    1.14 +  equation: thmdecl? prop comment?
    1.15 +  ;
    1.16 +  hints: ('congs' thmrefs)? ('simpset' name)?
    1.17    ;
    1.18  \end{rail}
    1.19  
    1.20 @@ -149,6 +154,12 @@
    1.21  $\isarkeyword{primrec}$ are that of the datatypes involved, while those of
    1.22  $\isarkeyword{recdef}$ are numbered (starting from $1$).
    1.23  
    1.24 +The equations provided by these packages may be referred later as theorem list
    1.25 +$f\mathord.simps$, where $f$ is the (collective) name of the functions
    1.26 +defined.  Individual equations may be named explicitly as well; note that for
    1.27 +$\isarkeyword{recdef}$ each specification given by the user may result in
    1.28 +several theorems.
    1.29 +
    1.30  See \cite{isabelle-HOL} for further information on recursive function
    1.31  definitions in HOL.
    1.32