avoid use of bin_rec_PM
authorhuffman
Thu, 23 Aug 2007 23:34:51 +0200
changeset 24416 0ca0c958c434
parent 24415 640b85390ba0
child 24417 5c3858b71f80
avoid use of bin_rec_PM
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)"