doc-src/IsarRef/hol.tex
 changeset 9751 1287787744a7 parent 9695 ec7d7f877712 child 9800 221388d5696d
equal inserted replaced
9750:270cd9831e7b 9751:1287787744a7
144   datatypes.
144   datatypes.
145 \item [$\isarkeyword{recdef}$] defines general well-founded recursive
145 \item [$\isarkeyword{recdef}$] defines general well-founded recursive
146   functions (using the TFL package).
146   functions (using the TFL package).
147 \end{descr}
147 \end{descr}
148
148
149 Both definitions accommodate reasoning proof by induction (cf.\
149 Both definitions accommodate reasoning by induction (cf.\
150 \S\ref{sec:induct-method}): rule $c\mathord{.}induct$ (where $c$ is the name
150 \S\ref{sec:induct-method}): rule $c\mathord{.}induct$ (where $c$ is the name
151 of the function definition) refers to a specific induction rule, with
151 of the function definition) refers to a specific induction rule, with
152 parameters named according to the user-specified equations.  Case names of
152 parameters named according to the user-specified equations.  Case names of
153 $\isarkeyword{primrec}$ are that of the datatypes involved, while those of
153 $\isarkeyword{primrec}$ are that of the datatypes involved, while those of
154 $\isarkeyword{recdef}$ are numbered (starting from $1$).
154 $\isarkeyword{recdef}$ are numbered (starting from $1$).