doc-src/TutorialI/Recdef/termination.thy

--- a/doc-src/TutorialI/Recdef/termination.thy	Fri Sep 28 20:08:05 2001 +0200
+++ b/doc-src/TutorialI/Recdef/termination.thy	Fri Sep 28 20:08:28 2001 +0200
@@ -17,7 +17,7 @@
 recursive call.  Let us try the following artificial function:*}
 
 consts f :: "nat\<times>nat \<Rightarrow> nat"
-recdef (*<*)(permissive)(*<*)f "measure(\<lambda>(x,y). x-y)"
+recdef (*<*)(permissive)(*>*)f "measure(\<lambda>(x,y). x-y)"
   "f(x,y) = (if x \<le> y then x else f(x,y+1))"
 
 text{*\noindent