# HG changeset patch
# User haftmann
# Date 1591299530 0
# Node ID a238074c5a9d8c4468196025e716c6de2e372597
# Parent  b0da0537f3077c15c378394f8101f668cc7e81bf
avoid overaggressive default simp rules

diff -r b0da0537f307 -r a238074c5a9d src/HOL/ex/Bit_Operations.thy
--- a/src/HOL/ex/Bit_Operations.thy	Thu Jun 04 15:30:22 2020 +0000
+++ b/src/HOL/ex/Bit_Operations.thy	Thu Jun 04 19:38:50 2020 +0000
@@ -57,11 +57,11 @@
   "a AND 0 = 0"
   by (simp add: bit_eq_iff bit_and_iff)
 
-lemma one_and_eq [simp]:
+lemma one_and_eq:
   "1 AND a = a mod 2"
   by (simp add: bit_eq_iff bit_and_iff) (auto simp add: bit_1_iff)
 
-lemma and_one_eq [simp]:
+lemma and_one_eq:
   "a AND 1 = a mod 2"
   using one_and_eq [of a] by (simp add: ac_simps)
 
diff -r b0da0537f307 -r a238074c5a9d src/HOL/ex/Word.thy
--- a/src/HOL/ex/Word.thy	Thu Jun 04 15:30:22 2020 +0000
+++ b/src/HOL/ex/Word.thy	Thu Jun 04 19:38:50 2020 +0000
@@ -721,14 +721,14 @@
 
 lemma even_word_iff [code]:
   \<open>even_word a \<longleftrightarrow> a AND 1 = 0\<close>
-  by (simp add: even_word_def even_iff_mod_2_eq_zero)
+  by (simp add: even_word_def and_one_eq even_iff_mod_2_eq_zero)
 
 definition bit_word :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> bool\<close>
   where [code_abbrev]: \<open>bit_word = bit\<close>
 
 lemma bit_word_iff [code]:
   \<open>bit_word a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close>
-  by (simp add: bit_word_def bit_iff_odd_drop_bit odd_iff_mod_2_eq_one)
+  by (simp add: bit_word_def bit_iff_odd_drop_bit and_one_eq odd_iff_mod_2_eq_one)
 
 lifting_update word.lifting
 lifting_forget word.lifting