diff -r fd242f857508 -r 0bec857c9871 doc-src/TutorialI/Advanced/WFrec.thy --- a/doc-src/TutorialI/Advanced/WFrec.thy Fri Sep 28 20:08:05 2001 +0200 +++ b/doc-src/TutorialI/Advanced/WFrec.thy Fri Sep 28 20:08:28 2001 +0200 @@ -67,7 +67,7 @@ *} consts f :: "nat \ nat" -recdef (*<*)(permissive)(*<*)f "{(i,j). j i \ (#10::nat)}" +recdef (*<*)(permissive)(*>*)f "{(i,j). j i \ (#10::nat)}" "f i = (if #10 \ i then 0 else i * f(Suc i))" text{*\noindent