src/HOL/ex/Termination.thy
changeset 33468 91ea7115da1b
parent 32399 4dc441c71cce
child 41413 64cd30d6b0b8
     1.1 --- a/src/HOL/ex/Termination.thy	Fri Nov 06 12:13:45 2009 +0100
     1.2 +++ b/src/HOL/ex/Termination.thy	Fri Nov 06 13:36:46 2009 +0100
     1.3 @@ -168,7 +168,7 @@
     1.4  
     1.5  
     1.6  
     1.7 -subsection {* Refined analysis: The @{text sizechange} method *}
     1.8 +subsection {* Refined analysis: The @{text size_change} method *}
     1.9  
    1.10  text {* Unsolvable for @{text lexicographic_order} *}
    1.11  
    1.12 @@ -179,7 +179,7 @@
    1.13  | "fun1 (Suc a, 0) = 0"
    1.14  | "fun1 (Suc a, Suc b) = fun1 (b, a)"
    1.15  by pat_completeness auto
    1.16 -termination by sizechange
    1.17 +termination by size_change
    1.18  
    1.19  
    1.20  text {* 
    1.21 @@ -195,7 +195,7 @@
    1.22  | "oprod x y z = eprod x (y - 1) (z+x)"
    1.23  | "eprod x y z = (if y=0 then z else prod (2*x) (y div 2) z)"
    1.24  by pat_completeness auto
    1.25 -termination by sizechange
    1.26 +termination by size_change
    1.27  
    1.28  text {* 
    1.29    Permutations of arguments:
    1.30 @@ -207,7 +207,7 @@
    1.31                    else if n > 0 then perm r (n - 1) m
    1.32                    else m)"
    1.33  by auto
    1.34 -termination by sizechange
    1.35 +termination by size_change
    1.36  
    1.37  text {*
    1.38    Artificial examples and regression tests:
    1.39 @@ -227,6 +227,6 @@
    1.40             0
    1.41        )"
    1.42  by pat_completeness auto
    1.43 -termination by sizechange -- {* requires Multiset *}
    1.44 +termination by size_change -- {* requires Multiset *}
    1.45  
    1.46  end