--- 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: *)
--- 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
--- 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>