| changeset 11636 | 0bec857c9871 |
| parent 11626 | 0dbfb578bf75 |
| child 11705 | ac8ca15c556c |
--- 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 \<Rightarrow> nat" -recdef (*<*)(permissive)(*<*)f "{(i,j). j<i \<and> i \<le> (#10::nat)}" +recdef (*<*)(permissive)(*>*)f "{(i,j). j<i \<and> i \<le> (#10::nat)}" "f i = (if #10 \<le> i then 0 else i * f(Suc i))" text{*\noindent