author | wenzelm |
Wed, 06 Jun 2018 11:41:37 +0200 | |
changeset 68389 | 1c84a8c513af |
parent 68388 | eb9d7e8708d5 |
child 68390 | c558a2202f32 |
--- a/src/HOL/Parity.thy Wed Jun 06 11:27:27 2018 +0200 +++ b/src/HOL/Parity.thy Wed Jun 06 11:41:37 2018 +0200 @@ -933,7 +933,7 @@ 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