--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Fri Nov 06 12:13:45 2009 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Fri Nov 06 13:36:46 2009 +0100
@@ -418,7 +418,7 @@
(Args.$$$ "ms" >> K MS))
|| Scan.succeed [MAX, MS, MIN]
-val setup = Method.setup @{binding sizechange}
+val setup = Method.setup @{binding size_change}
(Scan.lift orders --| Method.sections clasimp_modifiers >> decomp_scnp)
"termination prover with graph decomposition and the NP subset of size change termination"
--- a/src/HOL/ex/Termination.thy Fri Nov 06 12:13:45 2009 +0100
+++ b/src/HOL/ex/Termination.thy Fri Nov 06 13:36:46 2009 +0100
@@ -168,7 +168,7 @@
-subsection {* Refined analysis: The @{text sizechange} method *}
+subsection {* Refined analysis: The @{text size_change} method *}
text {* Unsolvable for @{text lexicographic_order} *}
@@ -179,7 +179,7 @@
| "fun1 (Suc a, 0) = 0"
| "fun1 (Suc a, Suc b) = fun1 (b, a)"
by pat_completeness auto
-termination by sizechange
+termination by size_change
text {*
@@ -195,7 +195,7 @@
| "oprod x y z = eprod x (y - 1) (z+x)"
| "eprod x y z = (if y=0 then z else prod (2*x) (y div 2) z)"
by pat_completeness auto
-termination by sizechange
+termination by size_change
text {*
Permutations of arguments:
@@ -207,7 +207,7 @@
else if n > 0 then perm r (n - 1) m
else m)"
by auto
-termination by sizechange
+termination by size_change
text {*
Artificial examples and regression tests:
@@ -227,6 +227,6 @@
0
)"
by pat_completeness auto
-termination by sizechange -- {* requires Multiset *}
+termination by size_change -- {* requires Multiset *}
end