--- a/src/HOL/Parity.thy Mon Nov 30 17:00:35 2020 +0100
+++ b/src/HOL/Parity.thy Mon Nov 30 17:10:49 2020 +0100
@@ -1197,7 +1197,7 @@
lemma bit_of_bool_iff [bit_simps]:
\<open>bit (of_bool b) n \<longleftrightarrow> b \<and> n = 0\<close>
- by (simp add: bit_1_iff)
+ by (simp add: bit_1_iff)
lemma even_of_nat_iff:
\<open>even (of_nat n) \<longleftrightarrow> even n\<close>
@@ -1536,7 +1536,7 @@
proof
assume ?P
then show ?Q
- by (simp add: take_bit_eq_mod mod_0_imp_dvd)
+ by (simp add: take_bit_eq_mod mod_0_imp_dvd)
next
assume ?Q
then obtain b where \<open>a = push_bit n b\<close>