changeset 11480 | 0fba0357c04c |
parent 11458 | 09a6c44a48ea |
child 11705 | ac8ca15c556c |
--- a/doc-src/TutorialI/Recdef/examples.thy Wed Aug 08 14:33:10 2001 +0200 +++ b/doc-src/TutorialI/Recdef/examples.thy Wed Aug 08 14:50:28 2001 +0200 @@ -9,7 +9,7 @@ consts fib :: "nat \<Rightarrow> nat"; recdef fib "measure(\<lambda>n. n)" "fib 0 = 0" - "fib 1 = 1" + "fib 1' = 1" "fib (Suc(Suc x)) = fib x + fib (Suc x)"; text{*\noindent