# HG changeset patch
# User huffman
# Date 1203124087 -3600
# Node ID b9c716a9fb5f6d5d3c97d102d9828bedb6dd2478
# Parent  815f3ccc0b454ea6985b4cace9ca15da4eecd805
added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps

diff -r 815f3ccc0b45 -r b9c716a9fb5f src/HOL/Real/Float.thy
--- a/src/HOL/Real/Float.thy	Sat Feb 16 02:01:13 2008 +0100
+++ b/src/HOL/Real/Float.thy	Sat Feb 16 02:08:07 2008 +0100
@@ -504,13 +504,9 @@
 lemma not_true_eq_false: "(~ True) = False" by simp
 
 lemmas binarith =
-  Pls_0_eq Min_1_eq
-  pred_Pls pred_Min pred_1 pred_0
-  succ_Pls succ_Min succ_1 succ_0
-  add_Pls add_Min add_BIT_0 add_BIT_10
-  add_BIT_11 minus_Pls minus_Min minus_1
-  minus_0 mult_Pls mult_Min mult_num1 mult_num0
-  add_Pls_right add_Min_right
+  normalize_bin_simps
+  pred_bin_simps succ_bin_simps
+  add_bin_simps minus_bin_simps mult_bin_simps
 
 lemma int_eq_number_of_eq:
   "(((number_of v)::int)=(number_of w)) = iszero ((number_of (v + uminus w))::int)"