# HG changeset patch
# User huffman
# Date 1228941095 28800
# Node ID 773098b76201be0d3394742344004483a7ea3f62
# Parent  3c8f483337319b70b4d75881300169e65eb76831
clean up diff_bin_simps

diff -r 3c8f48333731 -r 773098b76201 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Wed Dec 10 07:52:54 2008 -0800
+++ b/src/HOL/Int.thy	Wed Dec 10 12:31:35 2008 -0800
@@ -761,41 +761,18 @@
 
 text {* Subtraction *}
 
-lemma diff_Pls:
-  "Pls - k = - k"
-  unfolding numeral_simps by simp
-
-lemma diff_Min:
-  "Min - k = pred (- k)"
-  unfolding numeral_simps by simp
-
-lemma diff_Bit0_Bit0:
+lemma diff_bin_simps [simp]:
+  "k - Pls = k"
+  "k - Min = succ k"
+  "Pls - (Bit0 l) = Bit0 (Pls - l)"
+  "Pls - (Bit1 l) = Bit1 (Min - l)"
+  "Min - (Bit0 l) = Bit1 (Min - l)"
+  "Min - (Bit1 l) = Bit0 (Min - l)"
   "(Bit0 k) - (Bit0 l) = Bit0 (k - l)"
-  unfolding numeral_simps by simp
-
-lemma diff_Bit0_Bit1:
   "(Bit0 k) - (Bit1 l) = Bit1 (pred k - l)"
-  unfolding numeral_simps by simp
-
-lemma diff_Bit1_Bit0:
   "(Bit1 k) - (Bit0 l) = Bit1 (k - l)"
-  unfolding numeral_simps by simp
-
-lemma diff_Bit1_Bit1:
   "(Bit1 k) - (Bit1 l) = Bit0 (k - l)"
-  unfolding numeral_simps by simp
-
-lemma diff_Pls_right:
-  "k - Pls = k"
-  unfolding numeral_simps by simp
-
-lemma diff_Min_right:
-  "k - Min = succ k"
-  unfolding numeral_simps by simp
-
-lemmas diff_bin_simps [simp] =
-  diff_Pls diff_Min diff_Pls_right diff_Min_right
-  diff_Bit0_Bit0 diff_Bit0_Bit1 diff_Bit1_Bit0 diff_Bit1_Bit1
+  unfolding numeral_simps by simp_all
 
 text {* Multiplication *}