fixed manual (rule no longer exists)
authorkrauss
Fri, 25 Feb 2011 17:11:05 +0100
changeset 41847 b0d6acf73588
parent 41846 b368a7aee46a
child 41848 f53e0e0baa4f
fixed manual (rule no longer exists)
doc-src/Functions/Thy/Functions.thy
--- 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