doc-src/Functions/Thy/Functions.thy

 
 function (*<*)(domintros)(*>*)findzero :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat"
 where
   "findzero f n = (if f n = 0 then n else findzero f (Suc n))"
 by pat_completeness auto
-(*<*)declare findzero.simps[simp del](*>*)
 
 text {*
   \noindent Clearly, any attempt of a termination proof must fail. And without
   that, we do not get the usual rules @{text "findzero.simps"} and 
   @{text "findzero.induct"}. So what was the definition good for at all?