# HG changeset patch
# User wenzelm
# Date 978553357 -3600
# Node ID 662727d4ecac13fdb211fa6380befd255903cd4c
# Parent  4858ad0b8f3888eb391ce0be5ef6c79ef0ba5fe9
added 'recdef_tc' command;

diff -r 4858ad0b8f38 -r 662727d4ecac doc-src/IsarRef/hol.tex
--- 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.\