diff -r cd8acf137c9c -r 14a658faadb6 doc-src/Functions/Thy/document/Functions.tex
--- a/doc-src/Functions/Thy/document/Functions.tex	Mon Nov 23 15:05:59 2009 +0100
+++ b/doc-src/Functions/Thy/document/Functions.tex	Mon Nov 23 15:06:34 2009 +0100
@@ -453,9 +453,33 @@
   \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.
+  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}
 
-%  As a more real example, here is quicksort:%
+  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%
 %