doc-src/IsarAdvanced/Functions/Thy/Functions.thy
changeset 26580 c3e597a476fd
parent 25688 6c24a82a98f1
child 26749 397a1aeede7d
     1.1 --- a/doc-src/IsarAdvanced/Functions/Thy/Functions.thy	Tue Apr 08 15:47:15 2008 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Functions/Thy/Functions.thy	Tue Apr 08 18:30:40 2008 +0200
     1.3 @@ -595,12 +595,12 @@
     1.4    This is an arithmetic triviality, but unfortunately the
     1.5    @{text arith} method cannot handle this specific form of an
     1.6    elimination rule. However, we can use the method @{text
     1.7 -  "elim_to_cases"} to do an ad-hoc conversion to a disjunction of
     1.8 +  "atomize_elim"} to do an ad-hoc conversion to a disjunction of
     1.9    existentials, which can then be soved by the arithmetic decision procedure.
    1.10    Pattern compatibility and termination are automatic as usual.
    1.11  *}
    1.12  (*<*)ML "goals_limit := 10"(*>*)
    1.13 -apply elim_to_cases
    1.14 +apply atomize_elim
    1.15  apply arith
    1.16  apply auto
    1.17  done
    1.18 @@ -616,7 +616,7 @@
    1.19  where
    1.20    "ev (2 * n) = True"
    1.21  | "ev (2 * n + 1) = False"
    1.22 -apply elim_to_cases
    1.23 +apply atomize_elim
    1.24  by arith+
    1.25  termination by (relation "{}") simp
    1.26  
    1.27 @@ -649,7 +649,7 @@
    1.28  | "gcd 0 y = y"
    1.29  | "x < y \<Longrightarrow> gcd (Suc x) (Suc y) = gcd (Suc x) (y - x)"
    1.30  | "\<not> x < y \<Longrightarrow> gcd (Suc x) (Suc y) = gcd (x - y) (Suc y)"
    1.31 -by (elim_to_cases, auto, arith)
    1.32 +by (atomize_elim, auto, arith)
    1.33  termination by lexicographic_order
    1.34  
    1.35  text {*