doc-src/Functions/Thy/document/Functions.tex

   recursive call, and for the first argument nothing could be proved,
   which is expressed by \isa{{\isacharquery}}. In general, there are the values
   \isa{{\isacharless}}, \isa{{\isacharless}{\isacharequal}} and \isa{{\isacharquery}}.
 
   For the failed proof attempts, the unfinished subgoals are also
-  printed. Looking at these will often point to a missing lemma.
-
-%  As a more real example, here is quicksort:%
+  printed. Looking at these will often point to a missing lemma.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{The \isa{size{\isacharunderscore}change} method%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Some termination goals that are beyond the powers of
+  \isa{lexicographic{\isacharunderscore}order} can be solved automatically by the
+  more powerful \isa{size{\isacharunderscore}change} method, which uses a variant of
+  the size-change principle, together with some other
+  techniques. While the details are discussed
+  elsewhere\cite{krauss_phd},
+  here are a few typical situations where
+  \isa{lexicographic{\isacharunderscore}order} has difficulties and \isa{size{\isacharunderscore}change}
+  may be worth a try:
+  \begin{itemize}
+  \item Arguments are permuted in a recursive call.
+  \item Several mutually recursive functions with multiple arguments.
+  \item Unusual control flow (e.g., when some recursive calls cannot
+  occur in sequence).
+  \end{itemize}
+
+  Loading the theory \isa{Multiset} makes the \isa{size{\isacharunderscore}change}
+  method a bit stronger: it can then use multiset orders internally.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isamarkupsection{Mutual Recursion%
 }