# HG changeset patch
# User krauss
# Date 1258985198 -3600
# Node ID 0c348f7997f76d50f20162d76ec47cf8887f4fc5
# Parent  0cb5002c52dbcdc5c7eb724de0cc43d71225cf66
documented size_change in isar-ref manual

diff -r 0cb5002c52db -r 0c348f7997f7 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Nov 23 15:06:37 2009 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Nov 23 15:06:38 2009 +0100
@@ -506,6 +506,7 @@
     @{method_def (HOL) pat_completeness} & : & @{text method} \\
     @{method_def (HOL) relation} & : & @{text method} \\
     @{method_def (HOL) lexicographic_order} & : & @{text method} \\
+    @{method_def (HOL) size_change} & : & @{text method} \\
   \end{matharray}
 
   \begin{rail}
@@ -513,6 +514,9 @@
     ;
     'lexicographic\_order' ( clasimpmod * )
     ;
+    'size\_change' ( orders ( clasimpmod * ) )
+    ;
+    orders: ( 'max' | 'min' | 'ms' ) *
   \end{rail}
 
   \begin{description}
@@ -540,6 +544,18 @@
   In case of failure, extensive information is printed, which can help
   to analyse the situation (cf.\ \cite{isabelle-function}).
 
+  \item @{method (HOL) "size_change"} also works on termination goals,
+  using a variation of the size-change principle, together with a
+  graph decomposition technique (see \cite{krauss_phd} for details).
+  Three kinds of orders are used internally: @{text max}, @{text min},
+  and @{text ms} (multiset), which is only available when the theory
+  @{text Multiset} is loaded. When no order kinds are given, they are
+  tried in order. The search for a termination proof uses SAT solving
+  internally.
+
+ For local descent proofs, the same context modifiers as for @{method
+  auto} are accepted, see \secref{sec:clasimp}.
+
   \end{description}
 *}
 
diff -r 0cb5002c52db -r 0c348f7997f7 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Nov 23 15:06:37 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Nov 23 15:06:38 2009 +0100
@@ -512,6 +512,7 @@
     \indexdef{HOL}{method}{pat\_completeness}\hypertarget{method.HOL.pat-completeness}{\hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}}} & : & \isa{method} \\
     \indexdef{HOL}{method}{relation}\hypertarget{method.HOL.relation}{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}} & : & \isa{method} \\
     \indexdef{HOL}{method}{lexicographic\_order}\hypertarget{method.HOL.lexicographic-order}{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}}} & : & \isa{method} \\
+    \indexdef{HOL}{method}{size\_change}\hypertarget{method.HOL.size-change}{\hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isacharunderscore}change}}}} & : & \isa{method} \\
   \end{matharray}
 
   \begin{rail}
@@ -519,6 +520,9 @@
     ;
     'lexicographic\_order' ( clasimpmod * )
     ;
+    'size\_change' ( orders ( clasimpmod * ) )
+    ;
+    orders: ( 'max' | 'min' | 'ms' ) *
   \end{rail}
 
   \begin{description}
@@ -546,6 +550,17 @@
   In case of failure, extensive information is printed, which can help
   to analyse the situation (cf.\ \cite{isabelle-function}).
 
+  \item \hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isacharunderscore}change}}} also works on termination goals,
+  using a variation of the size-change principle, together with a
+  graph decomposition technique (see \cite{krauss_phd} for details).
+  Three kinds of orders are used internally: \isa{max}, \isa{min},
+  and \isa{ms} (multiset), which is only available when the theory
+  \isa{Multiset} is loaded. When no order kinds are given, they are
+  tried in order. The search for a termination proof uses SAT solving
+  internally.
+
+ For local descent proofs, the same context modifiers as for \hyperlink{method.auto}{\mbox{\isa{auto}}} are accepted, see \secref{sec:clasimp}.
+
   \end{description}%
 \end{isamarkuptext}%
 \isamarkuptrue%