src/HOL/Word/Bit_Representation.thy

   zmod_uminus' [symmetric]
   mod_add_left_eq [where b = "1::int"]
   zmod_zsub_left_eq [where b = "1"]
 
 lemmas bintr_arith1s =
-  brdmod1s' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p] for n
+  brdmod1s' [where c="2^n::int", folded bintrunc_mod2p] for n
 lemmas bintr_ariths =
-  brdmods' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p] for n
+  brdmods' [where c="2^n::int", folded bintrunc_mod2p] for n
 
 lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p]
 
 lemma bintr_ge0: "(0 :: int) <= number_of (bintrunc n w)"
   by (simp add : no_bintr m2pths)