--- a/doc-src/IsarRef/hol.tex Fri Sep 28 19:23:58 2001 +0200
+++ b/doc-src/IsarRef/hol.tex Fri Sep 28 19:24:25 2001 +0200
@@ -166,7 +166,7 @@
\begin{rail}
'primrec' parname? (equation + )
;
- 'recdef' name term (eqn + ) hints?
+ 'recdef' ('(' 'permissive' ')')? \\ name term (eqn + ) hints?
;
recdeftc thmdecl? tc comment?
;
@@ -188,11 +188,13 @@
datatypes, see also \cite{isabelle-HOL}.
\item [$\isarkeyword{recdef}$] defines general well-founded recursive
functions (using the TFL package), see also \cite{isabelle-HOL}. The
- $recdef_simp$, $recdef_cong$, and $recdef_wf$ hints refer to auxiliary rules
- to be used in the internal automated proof process of TFL. Additional
- $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}).
+ $(permissive)$ option tells TFL to recover from failed proof attempts,
+ returning unfinished results. The $recdef_simp$, $recdef_cong$, and
+ $recdef_wf$ hints refer to auxiliary rules to be used in the internal
+ automated proof process of TFL. Additional $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$.
@@ -259,7 +261,7 @@
sets: (term comment? +)
;
- intros: 'intros' attributes? (thmdecl? prop comment? +)
+ intros: 'intros' (thmdecl? prop comment? +)
;
monos: 'monos' thmrefs comment?
;