diff -r 4d4521cbbcca -r ca761fe227d8 src/HOL/Real/RealBin.ML
--- a/src/HOL/Real/RealBin.ML	Wed Jun 07 12:07:07 2000 +0200
+++ b/src/HOL/Real/RealBin.ML	Wed Jun 07 12:14:18 2000 +0200
@@ -13,7 +13,7 @@
 qed "real_number_of";
 Addsimps [real_number_of];
 
-Goalw [real_number_of_def] "0r = #0";
+Goalw [real_number_of_def] "(0::real) = #0";
 by (simp_tac (simpset() addsimps [real_of_int_zero RS sym]) 1);
 qed "zero_eq_numeral_0";
 
@@ -109,14 +109,14 @@
 
 Addsimps [le_real_number_of_eq_not_less];
 
-(*** New versions of existing theorems involving 0r, 1r ***)
+(*** New versions of existing theorems involving 0, 1r ***)
 
 Goal "- #1 = (#-1::real)";
 by (Simp_tac 1);
 qed "minus_numeral_one";
 
 
-(*Maps 0r to #0 and 1r to #1 and -1r to #-1*)
+(*Maps 0 to #0 and 1r to #1 and -1r to #-1*)
 val real_numeral_ss = 
     HOL_ss addsimps [zero_eq_numeral_0, one_eq_numeral_1, 
 		     minus_numeral_one];
@@ -124,7 +124,7 @@
 fun rename_numerals thy th = simplify real_numeral_ss (change_theory thy th);
 
 
-(*Now insert some identities previously stated for 0r and 1r*)
+(*Now insert some identities previously stated for 0 and 1r*)
 
 (** RealDef & Real **)
 
@@ -136,6 +136,17 @@
 	   real_mult_minus_1_right, real_mult_minus_1, real_rinv_1,
 	   real_minus_zero_less_iff]);
 
+AddIffs (map (rename_numerals thy) [real_mult_is_0, real_0_is_mult]);
+
+bind_thm ("real_0_less_times_iff", 
+	  rename_numerals thy real_zero_less_times_iff);
+bind_thm ("real_0_le_times_iff", 
+	  rename_numerals thy real_zero_le_times_iff);
+bind_thm ("real_times_less_0_iff", 
+	  rename_numerals thy real_times_less_zero_iff);
+bind_thm ("real_times_le_0_iff", 
+	  rename_numerals thy real_times_le_zero_iff);
+
 
 (*Perhaps add some theorems that aren't in the default simpset, as
   done in Integ/NatBin.ML*)
@@ -201,3 +212,27 @@
     asm_full_simplify real_numeral_ss (change_theory thy th);
 
 
+(** Simplification of arithmetic when nested to the right **)
+
+Goal "number_of v + (number_of w + z) = (number_of(bin_add v w) + z::real)";
+by Auto_tac; 
+qed "real_add_number_of_left";
+
+Goal "number_of v * (number_of w * z) = (number_of(bin_mult v w) * z::real)";
+by (simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1);
+qed "real_mult_number_of_left";
+
+Goalw [real_diff_def]
+    "number_of v + (number_of w - c) = number_of(bin_add v w) - (c::real)";
+by (rtac real_add_number_of_left 1);
+qed "real_add_number_of_diff1";
+
+Goal "number_of v + (c - number_of w) = \
+\    number_of (bin_add v (bin_minus w)) + (c::real)";
+by (stac (diff_real_number_of RS sym) 1);
+by Auto_tac;
+qed "real_add_number_of_diff2";
+
+Addsimps [real_add_number_of_left, real_mult_number_of_left,
+	  real_add_number_of_diff1, real_add_number_of_diff2]; 
+