--- a/src/HOL/Library/Bit_Operations.thy Mon Nov 30 17:00:35 2020 +0100
+++ b/src/HOL/Library/Bit_Operations.thy Mon Nov 30 17:10:49 2020 +0100
@@ -161,7 +161,7 @@
lemma or_eq_0_iff:
\<open>a OR b = 0 \<longleftrightarrow> a = 0 \<and> b = 0\<close>
- by (auto simp add: bit_eq_iff bit_or_iff)
+ by (auto simp add: bit_eq_iff bit_or_iff)
lemma disjunctive_add:
\<open>a + b = a OR b\<close> if \<open>\<And>n. \<not> bit a n \<or> \<not> bit b n\<close>
@@ -269,7 +269,7 @@
proof
assume \<open>a = - 1 \<and> b = - 1\<close>
then show \<open>a AND b = - 1\<close>
- by simp
+ by simp
next
assume \<open>a AND b = - 1\<close>
have *: \<open>bit a n\<close> \<open>bit b n\<close> if \<open>2 ^ n \<noteq> 0\<close> for n
@@ -278,7 +278,7 @@
have \<open>bit (a AND b) n = bit (- 1) n\<close>
by (simp add: bit_eq_iff)
then show \<open>bit a n\<close> \<open>bit b n\<close>
- using that by (simp_all add: bit_and_iff)
+ using that by (simp_all add: bit_and_iff)
qed
have \<open>a = - 1\<close>
by (rule bit_eqI) (simp add: *)