# HG changeset patch
# User haftmann
# Date 1588919187 0
# Node ID 541e68d1a964c31f9adc05168e936bd4a06655cd
# Parent  dd5b8072ca90ddb2670d27a1fb229f28c2a21768
less aggressive default simp rules

diff -r dd5b8072ca90 -r 541e68d1a964 src/HOL/ex/Bit_Operations.thy
--- a/src/HOL/ex/Bit_Operations.thy	Wed May 06 15:31:24 2020 +0200
+++ b/src/HOL/ex/Bit_Operations.thy	Fri May 08 06:26:27 2020 +0000
@@ -226,7 +226,7 @@
       (cases m, simp_all add: bit_Suc)
 qed
 
-lemma set_bit_Suc [simp]:
+lemma set_bit_Suc:
   \<open>set_bit (Suc n) a = a mod 2 + 2 * set_bit n (a div 2)\<close>
 proof (rule bit_eqI)
   fix m
@@ -257,7 +257,7 @@
       (cases m, simp_all add: bit_Suc)
 qed
 
-lemma unset_bit_Suc [simp]:
+lemma unset_bit_Suc:
   \<open>unset_bit (Suc n) a = a mod 2 + 2 * unset_bit n (a div 2)\<close>
 proof (rule bit_eqI)
   fix m
@@ -286,7 +286,7 @@
       (cases m, simp_all add: bit_Suc)
 qed
 
-lemma flip_bit_Suc [simp]:
+lemma flip_bit_Suc:
   \<open>flip_bit (Suc n) a = a mod 2 + 2 * flip_bit n (a div 2)\<close>
 proof (rule bit_eqI)
   fix m