src/HOL/Parity.thy

   by (simp only: numeral_eq_Suc power_Suc numeral_Bit1 [of k] mult_2 [symmetric] drop_bit_Suc
     div_mult_self4 [OF numeral_neq_zero]) simp
 
 lemma drop_bit_of_nat:
   "drop_bit n (of_nat m) = of_nat (drop_bit n m)"
-	by (simp add: drop_bit_eq_div Parity.drop_bit_eq_div of_nat_div [of m "2 ^ n"])
+  by (simp add: drop_bit_eq_div Parity.drop_bit_eq_div of_nat_div [of m "2 ^ n"])
 
 end
 
 lemma push_bit_of_Suc_0 [simp]:
   "push_bit n (Suc 0) = 2 ^ n"