doc-src/TutorialI/Types/Numbers.thy
changeset 44048 64f574163ca2
parent 38767 d8da44a8dd25
child 47183 f760e15343bc
     1.1 --- a/doc-src/TutorialI/Types/Numbers.thy	Mon Aug 08 07:13:16 2011 +0200
     1.2 +++ b/doc-src/TutorialI/Types/Numbers.thy	Mon Aug 08 07:35:42 2011 +0200
     1.3 @@ -16,8 +16,7 @@
     1.4  *};
     1.5  oops
     1.6  
     1.7 -consts h :: "nat \<Rightarrow> nat"
     1.8 -recdef h "{}"
     1.9 +fun h :: "nat \<Rightarrow> nat" where
    1.10  "h i = (if i = 3 then 2 else i)"
    1.11  
    1.12  text{*