doc-src/IsarRef/hol.tex
changeset 9751 1287787744a7
parent 9695 ec7d7f877712
child 9800 221388d5696d
equal deleted 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$).