# HG changeset patch
# User krauss
# Date 1298650265 -3600
# Node ID b0d6acf73588c10133af9026a8c78c100e157a34
# Parent  b368a7aee46a94652e629081b5a14f9331f4166d
fixed manual (rule no longer exists)

diff -r b368a7aee46a -r b0d6acf73588 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