author | krauss |
Fri, 25 Feb 2011 17:11:05 +0100 | |
changeset 41847 | b0d6acf73588 |
parent 41846 | b368a7aee46a |
child 41848 | f53e0e0baa4f |
--- a/doc-src/Functions/Thy/Functions.thy Fri Feb 25 16:59:48 2011 +0100 +++ b/doc-src/Functions/Thy/Functions.thy Fri Feb 25 17:11:05 2011 +0100 @@ -706,7 +706,6 @@ 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