author krauss Fri, 06 Nov 2009 13:36:46 +0100 changeset 33468 91ea7115da1b parent 33467 c3971d3c6afd child 33469 0183f9545fa2
renamed method sizechange to size_change
```--- 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```