diff -r b79755daf0ad -r 26492b600d78 src/HOL/Library/Bit_Operations.thy
--- 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: *)