--- a/src/HOL/Library/ContNotDenum.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/Library/ContNotDenum.thy Mon Jul 12 08:58:13 2010 +0200
@@ -402,7 +402,6 @@
(f (Suc n)) \<notin> e)
)"
-declare newInt.simps [code del]
subsubsection {* Properties *}