# HG changeset patch
# User wenzelm
# Date 1606752649 -3600
# Node ID 26492b600d78fed403249d1f7b6181c2758e76a1
# Parent  b79755daf0add03973b620f3c67965af73c50bd9
tuned whitespace --- avoid TABs;

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: *)
diff -r b79755daf0ad -r 26492b600d78 src/HOL/Library/Type_Length.thy
--- a/src/HOL/Library/Type_Length.thy	Mon Nov 30 17:00:35 2020 +0100
+++ b/src/HOL/Library/Type_Length.thy	Mon Nov 30 17:10:49 2020 +0100
@@ -113,7 +113,7 @@
 lemma two_less_eq_exp_length [simp]:
   \<open>2 \<le> 2 ^ LENGTH('b::len)\<close>
   using mult_left_mono [of 1 \<open>2 ^ (LENGTH('b::len) - 1)\<close> 2]
-		  by (cases \<open>LENGTH('b::len)\<close>) simp_all
+  by (cases \<open>LENGTH('b::len)\<close>) simp_all
 
 end
 
diff -r b79755daf0ad -r 26492b600d78 src/HOL/Parity.thy
--- 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>