1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Nov 23 15:06:37 2009 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Nov 23 15:06:38 2009 +0100
     1.3 @@ -512,6 +512,7 @@
     1.4      \indexdef{HOL}{method}{pat\_completeness}\hypertarget{method.HOL.pat-completeness}{\hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}}} & : & \isa{method} \\
     1.5      \indexdef{HOL}{method}{relation}\hypertarget{method.HOL.relation}{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}} & : & \isa{method} \\
     1.6      \indexdef{HOL}{method}{lexicographic\_order}\hypertarget{method.HOL.lexicographic-order}{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}}} & : & \isa{method} \\
     1.7 +    \indexdef{HOL}{method}{size\_change}\hypertarget{method.HOL.size-change}{\hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isacharunderscore}change}}}} & : & \isa{method} \\
     1.8    \end{matharray}
     1.9  
    1.10    \begin{rail}
    1.11 @@ -519,6 +520,9 @@
    1.12      ;
    1.13      'lexicographic\_order' ( clasimpmod * )
    1.14      ;
    1.15 +    'size\_change' ( orders ( clasimpmod * ) )
    1.16 +    ;
    1.17 +    orders: ( 'max' | 'min' | 'ms' ) *
    1.18    \end{rail}
    1.19  
    1.20    \begin{description}
    1.21 @@ -546,6 +550,17 @@
    1.22    In case of failure, extensive information is printed, which can help
    1.23    to analyse the situation (cf.\ \cite{isabelle-function}).
    1.24  
    1.25 +  \item \hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isacharunderscore}change}}} also works on termination goals,
    1.26 +  using a variation of the size-change principle, together with a
    1.27 +  graph decomposition technique (see \cite{krauss_phd} for details).
    1.28 +  Three kinds of orders are used internally: \isa{max}, \isa{min},
    1.29 +  and \isa{ms} (multiset), which is only available when the theory
    1.30 +  \isa{Multiset} is loaded. When no order kinds are given, they are
    1.31 +  tried in order. The search for a termination proof uses SAT solving
    1.32 +  internally.
    1.33 +
    1.34 + For local descent proofs, the same context modifiers as for \hyperlink{method.auto}{\mbox{\isa{auto}}} are accepted, see \secref{sec:clasimp}.
    1.35 +
    1.36    \end{description}%
    1.37  \end{isamarkuptext}%
    1.38  \isamarkuptrue%