--- a/src/HOL/Word/BinOperations.thy Mon Aug 20 22:57:50 2007 +0200
+++ b/src/HOL/Word/BinOperations.thy Mon Aug 20 23:00:17 2007 +0200
@@ -236,7 +236,10 @@
apply (case_tac ba, auto)
done
+(*
+Why were these declared simp???
declare bin_ops_comm [simp] bbw_assocs [simp]
+*)
lemma plus_and_or [rule_format]:
"ALL y::int. (x AND y) + (x OR y) = x + y"
--- a/src/HOL/Word/WordBitwise.thy Mon Aug 20 22:57:50 2007 +0200
+++ b/src/HOL/Word/WordBitwise.thy Mon Aug 20 23:00:17 2007 +0200
@@ -74,7 +74,7 @@
using word_of_int_Ex [where x=x]
word_of_int_Ex [where x=y]
word_of_int_Ex [where x=z]
- by (auto simp: bwsimps)
+ by (auto simp: bwsimps bbw_assocs)
lemma word_bw_comms:
fixes x :: "'a::len0 word"
@@ -84,7 +84,7 @@
"x XOR y = y XOR x"
using word_of_int_Ex [where x=x]
word_of_int_Ex [where x=y]
- by (auto simp: bwsimps)
+ by (auto simp: bwsimps bin_ops_comm)
lemma word_bw_lcs:
fixes x :: "'a::len0 word"