# HG changeset patch
# User wenzelm
# Date 1001697865 -7200
# Node ID cddf6441a14adbf6ef6bee197ae521b2a265f26e
# Parent  c8945e0dc00bfe3f227d225cdcf3a11190f852ff
recdef (permissive);
inductive: no collective atts;

diff -r c8945e0dc00b -r cddf6441a14a doc-src/IsarRef/hol.tex
--- 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?
   ;