# HG changeset patch
# User huffman
# Date 1187904891 -7200
# Node ID 0ca0c958c43457c61ca2fed075710ce82ac6cf83
# Parent  640b85390ba03853cb07d51703aecd20e3e05720
avoid use of bin_rec_PM

diff -r 640b85390ba0 -r 0ca0c958c434 src/HOL/Word/BinOperations.thy
--- a/src/HOL/Word/BinOperations.thy	Thu Aug 23 20:15:45 2007 +0200
+++ b/src/HOL/Word/BinOperations.thy	Thu Aug 23 23:34:51 2007 +0200
@@ -36,11 +36,11 @@
 
 lemma int_xor_Pls [simp]: 
   "Numeral.Pls XOR x = x"
-  unfolding int_xor_def by (simp add: bin_rec_PM)
+  unfolding int_xor_def by (simp add: bin_rec_Pls)
 
 lemma int_xor_Min [simp]: 
   "Numeral.Min XOR x = NOT x"
-  unfolding int_xor_def by (simp add: bin_rec_PM)
+  unfolding int_xor_def by (simp add: bin_rec_Min)
 
 lemma int_xor_Bits [simp]: 
   "(x BIT b) XOR (y BIT c) = (x XOR y) BIT (b XOR c)"
@@ -66,11 +66,11 @@
 
 lemma int_or_Pls [simp]: 
   "Numeral.Pls OR x = x"
-  by (unfold int_or_def) (simp add: bin_rec_PM)
+  by (unfold int_or_def) (simp add: bin_rec_Pls)
   
 lemma int_or_Min [simp]:
   "Numeral.Min OR x = Numeral.Min"
-  by (unfold int_or_def) (simp add: bin_rec_PM)
+  by (unfold int_or_def) (simp add: bin_rec_Min)
 
 lemma int_or_Bits [simp]: 
   "(x BIT b) OR (y BIT c) = (x OR y) BIT (b OR c)"
@@ -90,11 +90,11 @@
 
 lemma int_and_Pls [simp]:
   "Numeral.Pls AND x = Numeral.Pls"
-  unfolding int_and_def by (simp add: bin_rec_PM)
+  unfolding int_and_def by (simp add: bin_rec_Pls)
 
 lemma int_and_Min [simp]:
   "Numeral.Min AND x = x"
-  unfolding int_and_def by (simp add: bin_rec_PM)
+  unfolding int_and_def by (simp add: bin_rec_Min)
 
 lemma int_and_Bits [simp]: 
   "(x BIT b) AND (y BIT c) = (x AND y) BIT (b AND c)"