# HG changeset patch
# User huffman
# Date 1187643617 -7200
# Node ID 3e29eafabe165131252c41895f8476b92eec5bb3
# Parent  08b11604954756bf611779c20e45e53b213cef58
AC rules for bitwise logical operators no longer declared simp

diff -r 08b116049547 -r 3e29eafabe16 src/HOL/Word/BinOperations.thy
--- 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"
diff -r 08b116049547 -r 3e29eafabe16 src/HOL/Word/WordBitwise.thy
--- 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"