src/HOL/Library/ContNotDenum.thy
changeset 37765 26bdfb7b680b
parent 30663 0b6aff7451b2
child 40702 cf26dd7395e4
--- 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 *}