1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Sun Jun 05 20:23:05 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Sun Jun 05 22:02:54 2011 +0200
     1.3 @@ -520,9 +520,8 @@
     1.4    automated termination proof by searching for a lexicographic
     1.5    combination of size measures on the arguments of the function. The
     1.6    method accepts the same arguments as the @{method auto} method,
     1.7 -  which it uses internally to prove local descents.  The same context
     1.8 -  modifiers as for @{method auto} are accepted, see
     1.9 -  \secref{sec:clasimp}.
    1.10 +  which it uses internally to prove local descents.  The @{syntax
    1.11 +  clasimpmod} modifiers are accepted (as for @{method auto}).
    1.12  
    1.13    In case of failure, extensive information is printed, which can help
    1.14    to analyse the situation (cf.\ \cite{isabelle-function}).
    1.15 @@ -536,8 +535,8 @@
    1.16    tried in order. The search for a termination proof uses SAT solving
    1.17    internally.
    1.18  
    1.19 - For local descent proofs, the same context modifiers as for @{method
    1.20 -  auto} are accepted, see \secref{sec:clasimp}.
    1.21 +  For local descent proofs, the @{syntax clasimpmod} modifiers are
    1.22 +  accepted (as for @{method auto}).
    1.23  
    1.24    \end{description}
    1.25  *}
    1.26 @@ -647,9 +646,9 @@
    1.27    results.  The @{text recdef_simp}, @{text recdef_cong}, and @{text
    1.28    recdef_wf} hints refer to auxiliary rules to be used in the internal
    1.29    automated proof process of TFL.  Additional @{syntax clasimpmod}
    1.30 -  declarations (cf.\ \secref{sec:clasimp}) may be given to tune the
    1.31 -  context of the Simplifier (cf.\ \secref{sec:simplifier}) and
    1.32 -  Classical reasoner (cf.\ \secref{sec:classical}).
    1.33 +  declarations may be given to tune the context of the Simplifier
    1.34 +  (cf.\ \secref{sec:simplifier}) and Classical reasoner (cf.\
    1.35 +  \secref{sec:classical}).
    1.36  
    1.37    \item @{command (HOL) "recdef_tc"}~@{text "c (i)"} recommences the
    1.38    proof for leftover termination condition number @{text i} (default