# HG changeset patch
# User krauss
# Date 1257511006 -3600
# Node ID 91ea7115da1b16a96ece792323fecc683477757c
# Parent  c3971d3c6afd6f4b85ba15934e701c16c94659f4
renamed method sizechange to size_change

diff -r c3971d3c6afd -r 91ea7115da1b src/HOL/Tools/Function/scnp_reconstruct.ML
--- 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"
 
diff -r c3971d3c6afd -r 91ea7115da1b src/HOL/ex/Termination.thy
--- 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