# HG changeset patch
# User huffman
# Date 1332879026 -7200
# Node ID 80c4324042049c49d8f158f88a2125d16d005374
# Parent  3b5434efdf91717d88f58bae99a7f8ad496596d8
remove unnecessary rules from the simpset

diff -r 3b5434efdf91 -r 80c432404204 src/HOL/Word/Misc_Numeric.thy
--- a/src/HOL/Word/Misc_Numeric.thy	Tue Mar 27 21:58:41 2012 +0200
+++ b/src/HOL/Word/Misc_Numeric.thy	Tue Mar 27 22:10:26 2012 +0200
@@ -33,8 +33,8 @@
 
 lemma zless2: "0 < (2 :: int)" by arith
 
-lemmas zless2p [simp] = zless2 [THEN zero_less_power]
-lemmas zle2p [simp] = zless2p [THEN order_less_imp_le]
+lemmas zless2p = zless2 [THEN zero_less_power]
+lemmas zle2p = zless2p [THEN order_less_imp_le]
 
 lemmas pos_mod_sign2 = zless2 [THEN pos_mod_sign [where b = "2::int"]]
 lemmas pos_mod_bound2 = zless2 [THEN pos_mod_bound [where b = "2::int"]]