1.1 --- a/src/HOL/Word/Misc_Numeric.thy	Tue Mar 27 21:58:41 2012 +0200
     1.2 +++ b/src/HOL/Word/Misc_Numeric.thy	Tue Mar 27 22:10:26 2012 +0200
     1.3 @@ -33,8 +33,8 @@
     1.4  
     1.5  lemma zless2: "0 < (2 :: int)" by arith
     1.6  
     1.7 -lemmas zless2p [simp] = zless2 [THEN zero_less_power]
     1.8 -lemmas zle2p [simp] = zless2p [THEN order_less_imp_le]
     1.9 +lemmas zless2p = zless2 [THEN zero_less_power]
    1.10 +lemmas zle2p = zless2p [THEN order_less_imp_le]
    1.11  
    1.12  lemmas pos_mod_sign2 = zless2 [THEN pos_mod_sign [where b = "2::int"]]
    1.13  lemmas pos_mod_bound2 = zless2 [THEN pos_mod_bound [where b = "2::int"]]