src/HOL/FunDef.thy

--- a/src/HOL/FunDef.thy	Fri Apr 25 15:30:33 2008 +0200
+++ b/src/HOL/FunDef.thy	Fri Apr 25 16:28:06 2008 +0200
@@ -135,4 +135,10 @@
   "f (g x) = f' (g' x') \<Longrightarrow> (f o g) x = (f' o g') x'"
   unfolding o_apply .
 
+lemma termination_basic_simps[termination_simp]:
+  "x < y \<Longrightarrow> x < Suc y"
+  "x < (y::nat) \<Longrightarrow> x < y + z" 
+  "x < z \<Longrightarrow> x < y + z"
+by arith+
+
 end