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 {*
```