remove unnecessary simp rules involving Abs_Integ
authorhuffman
Wed, 30 May 2012 14:55:44 +0200
changeset 48044 fea6f3060b65
parent 48043 3ff2c76c9f64
child 48045 fbf77fdf9ae4
remove unnecessary simp rules involving Abs_Integ
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"