# HG changeset patch
# User huffman
# Date 1338382544 -7200
# Node ID fea6f3060b65a276d3e267a746224ffbc2c856b1
# Parent  3ff2c76c9f641142a53210610e515783a0d1e3d8
remove unnecessary simp rules involving Abs_Integ

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"