--- a/src/HOL/ex/Fundefs.thy Mon Nov 13 12:10:49 2006 +0100
+++ b/src/HOL/ex/Fundefs.thy Mon Nov 13 13:51:22 2006 +0100
@@ -17,8 +17,7 @@
| "fib (Suc 0) = 1"
| "fib (Suc (Suc n)) = fib n + fib (Suc n)"
-
-text {* we get partial simp and induction rules: *}
+text {* partial simp and induction rules: *}
thm fib.psimps
thm fib.pinduct
@@ -27,15 +26,10 @@
thm fib.domintros
-
-text {* Now termination: *}
-(*termination fib
- by (auto_term "less_than")*)
-
+text {* total simp and induction rules: *}
thm fib.simps
thm fib.induct
-
section {* Currying *}
fun add :: "nat \<Rightarrow> nat \<Rightarrow> nat"
@@ -62,8 +56,7 @@
by induct auto
termination nz
- apply (auto_term "less_than") -- {* Oops, it left us something to prove *}
- by (auto simp:nz_is_zero)
+ by (relation "less_than") (auto simp:nz_is_zero)
thm nz.simps
thm nz.induct