diff -r fd242f857508 -r 0bec857c9871 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\nat \ nat" -recdef (*<*)(permissive)(*<*)f "measure(\(x,y). x-y)" +recdef (*<*)(permissive)(*>*)f "measure(\(x,y). x-y)" "f(x,y) = (if x \ y then x else f(x,y+1))" text{*\noindent