
diff -r 3ff2c76c9f64 -r fea6f3060b65 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Wed May 30 23:10:42 2012 +0200
+++ b/src/HOL/Int.thy	Wed May 30 14:55:44 2012 +0200
@@ -870,11 +870,7 @@
 
 subsection{*The functions @{term nat} and @{term int}*}
 
-text{*Simplify the terms @{term "int 0"}, @{term "int(Suc 0)"} and
-  @{term "w + - z"}*}
-declare Zero_int_def [symmetric, simp]
-declare One_int_def [symmetric, simp]
-
+text{*Simplify the term @{term "w + - z"}*}
 lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp]
 
 lemma nat_0 [simp]: "nat 0 = 0"




