--- 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}
*}
--- 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%