--- a/doc-src/IsarRef/hol.tex Wed Jan 03 21:21:28 2001 +0100
+++ b/doc-src/IsarRef/hol.tex Wed Jan 03 21:22:37 2001 +0100
@@ -125,10 +125,11 @@
\section{Recursive functions}
-\indexisarcmd{primrec}\indexisarcmd{recdef}
+\indexisarcmd{primrec}\indexisarcmd{recdef}\indexisarcmd{recdef-tc}
\begin{matharray}{rcl}
\isarcmd{primrec} & : & \isartrans{theory}{theory} \\
\isarcmd{recdef} & : & \isartrans{theory}{theory} \\
+ \isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\
%FIXME
% \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\
\end{matharray}
@@ -142,11 +143,16 @@
\railalias{recdefwf}{recdef\_wf}
\railterm{recdefwf}
+\railalias{recdeftc}{recdef\_tc}
+\railterm{recdeftc}
+
\begin{rail}
'primrec' parname? (equation + )
;
'recdef' name term (eqn + ) hints?
;
+ recdeftc thmdecl? tc comment?
+ ;
equation: thmdecl? eqn
;
@@ -156,6 +162,8 @@
;
recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod
;
+ tc: nameref ('(' nat ')')?
+ ;
\end{rail}
\begin{descr}
@@ -168,6 +176,12 @@
$clasimpmod$ declarations (cf.\ \S\ref{sec:clasimp}) may be given to tune
the context of the Simplifier (cf.\ \S\ref{sec:simplifier}) and Classical
reasoner (cf.\ \S\ref{sec:classical}).
+\item [$\isarkeyword{recdef_tc}~c~(i)$] recommences the proof for leftover
+ termination condition number $i$ (default $1$) as generated by a
+ $\isarkeyword{recdef}$ definition of constant $c$.
+
+ Note that in most cases, $\isarkeyword{recdef}$ is able to finish its
+ internal proofs without manual intervention.
\end{descr}
Both kinds of recursive definitions accommodate reasoning by induction (cf.\