# HG changeset patch
# User paulson
# Date 960997638 -7200
# Node ID 15f82c9aa33187b646a1660d66cecc43a92b1a65
# Parent  eacebbcafe57d6bc4d07c11b4e36df324b21bd39
full_rename_numerals -> rename_numerals; tidied

diff -r eacebbcafe57 -r 15f82c9aa331 src/HOL/Real/RComplete.ML
--- a/src/HOL/Real/RComplete.ML	Wed Jun 14 17:46:10 2000 +0200
+++ b/src/HOL/Real/RComplete.ML	Wed Jun 14 17:47:18 2000 +0200
@@ -17,16 +17,16 @@
 Goal "ALL x:P. #0 < x ==> \ 
 \       ((EX x:P. y < x) = (EX X. real_of_preal X : P & \
 \                          y < real_of_preal X))";
-by (blast_tac (claset() addSDs [bspec,rename_numerals thy
-				real_gt_zero_preal_Ex RS iffD1]) 1);
+by (blast_tac (claset() addSDs [bspec, 
+		    rename_numerals thy real_gt_zero_preal_Ex RS iffD1]) 1);
 qed "real_sup_lemma1";
 
 Goal "[| ALL x:P. #0 < x; EX x. x: P; EX y. ALL x: P. x < y |] \
 \         ==> (EX X. X: {w. real_of_preal w : P}) & \
 \             (EX Y. ALL X: {w. real_of_preal w : P}. X < Y)";
 by (rtac conjI 1);
-by (blast_tac (claset() addDs [bspec, rename_numerals thy 
-    real_gt_zero_preal_Ex RS iffD1]) 1);
+by (blast_tac (claset() addDs [bspec, 
+                rename_numerals thy real_gt_zero_preal_Ex RS iffD1]) 1);
 by Auto_tac;
 by (dtac bspec 1 THEN assume_tac 1);
 by (ftac bspec 1  THEN assume_tac 1);
@@ -57,7 +57,7 @@
 by (ftac real_sup_lemma2 1 THEN Auto_tac);
 by (case_tac "#0 < ya" 1);
 by (dtac ((rename_numerals thy real_gt_zero_preal_Ex) RS iffD1) 1);
-by (dtac (full_rename_numerals thy real_less_all_real2) 2);
+by (dtac (rename_numerals thy real_less_all_real2) 2);
 by Auto_tac;
 by (rtac (preal_complete RS spec RS iffD1) 1);
 by Auto_tac;
@@ -66,9 +66,10 @@
 (* second part *)
 by (rtac (real_sup_lemma1 RS iffD2) 1 THEN assume_tac 1);
 by (case_tac "#0 < ya" 1);
-by (auto_tac (claset() addSDs (map (full_rename_numerals 
-    thy) [real_less_all_real2,real_gt_zero_preal_Ex RS iffD1]),
-    simpset()));
+by (auto_tac (claset() addSDs (map (rename_numerals thy) 
+			       [real_less_all_real2,
+				real_gt_zero_preal_Ex RS iffD1]),
+	      simpset()));
 by (ftac real_sup_lemma2 2 THEN Auto_tac);
 by (ftac real_sup_lemma2 1 THEN Auto_tac);
 by (rtac (preal_complete RS spec RS iffD2 RS bexE) 1);
@@ -104,8 +105,8 @@
 by (auto_tac (claset(), simpset() addsimps 
     [isLub_def,leastP_def,isUb_def]));
 by (auto_tac (claset() addSIs [setleI,setgeI] 
-     addSDs [(rename_numerals thy real_gt_zero_preal_Ex)
-     RS iffD1],simpset()));
+	         addSDs [(rename_numerals thy real_gt_zero_preal_Ex) RS iffD1],
+	      simpset()));
 by (forw_inst_tac [("x","y")] bspec 1 THEN assume_tac 1);
 by (dtac ((rename_numerals thy real_gt_zero_preal_Ex) RS iffD1) 1);
 by (auto_tac (claset(), simpset() addsimps [real_of_preal_le_iff]));
@@ -232,17 +233,15 @@
 by (res_inst_tac [("x","0")] exI 2);
 by (auto_tac (claset() addEs [real_less_trans],
 	      simpset() addsimps [real_of_posnat_one,real_zero_less_one]));
-by (forward_tac [((full_rename_numerals thy real_rinv_gt_zero)
-     RS reals_Archimedean)] 1);
+by (ftac ((rename_numerals thy real_rinv_gt_zero) RS reals_Archimedean) 1);
 by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1);
-by (forw_inst_tac [("y","rinv x")] 
-    (full_rename_numerals thy real_mult_less_mono1) 1);
+by (forw_inst_tac [("y","rinv x")]
+    (rename_numerals thy real_mult_less_mono1) 1);
 by (auto_tac (claset(),simpset() addsimps [real_not_refl2 RS not_sym]));
 by (dres_inst_tac [("n1","n"),("y","#1")] 
      (real_of_posnat_less_zero RS real_mult_less_mono2)  1);
 by (auto_tac (claset(),
-	      simpset() addsimps [rename_numerals thy 
-                                  real_of_posnat_less_zero,
+	      simpset() addsimps [rename_numerals thy real_of_posnat_less_zero,
 				  real_not_refl2 RS not_sym,
 				  real_mult_assoc RS sym]));
 qed "reals_Archimedean2";
diff -r eacebbcafe57 -r 15f82c9aa331 src/HOL/Real/RealAbs.ML
--- a/src/HOL/Real/RealAbs.ML	Wed Jun 14 17:46:10 2000 +0200
+++ b/src/HOL/Real/RealAbs.ML	Wed Jun 14 17:47:18 2000 +0200
@@ -88,15 +88,14 @@
 
 Goalw [abs_real_def] "abs (x * y) = abs x * abs (y::real)";
 by (auto_tac (claset() addSDs [order_antisym],
-	      simpset() addsimps [real_0_le_times_iff]));
+	      simpset() addsimps [real_0_le_mult_iff]));
 qed "abs_mult";
 
 Goalw [abs_real_def] "x~= (#0::real) ==> abs(rinv(x)) = rinv(abs(x))";
 by (auto_tac (claset(), 
               simpset() addsimps [real_le_less] @ 
-    (map (full_rename_numerals thy) [real_minus_rinv, real_rinv_gt_zero])));
-by (etac (full_rename_numerals thy (real_rinv_less_zero 
-    RSN (2,real_less_asym))) 1);
+	    (map (rename_numerals thy) [real_minus_rinv, real_rinv_gt_zero])));
+by (etac (rename_numerals thy (real_rinv_less_zero RSN (2,real_less_asym))) 1);
 by (arith_tac 1);
 qed "abs_rinv";
 
@@ -139,8 +138,8 @@
 qed "real_mult_0_less";
 
 Goal "[| (#0::real)<y; x<r; y*r<t*s |] ==> y*x<t*s";
-by (blast_tac (claset() addSIs [full_rename_numerals thy 
-    real_mult_less_mono2] addIs  [real_less_trans]) 1);
+by (blast_tac (claset() addSIs [rename_numerals thy real_mult_less_mono2] 
+                        addIs  [real_less_trans]) 1);
 qed "real_mult_less_trans";
 
 Goal "[| (#0::real)<=y; x<r; y*r<t*s; #0<t*s|] ==> y*x<t*s";
@@ -154,7 +153,7 @@
 by (rtac real_mult_le_less_trans 1);
 by (rtac abs_ge_zero 1);
 by (assume_tac 1);
-by (rtac (full_rename_numerals thy real_mult_order) 2);
+by (rtac (rename_numerals thy real_mult_order) 2);
 by (auto_tac (claset() addSIs [real_mult_less_mono1,
     abs_ge_zero] addIs [real_le_less_trans],simpset()));
 qed "abs_mult_less";
@@ -168,8 +167,8 @@
 by (cut_inst_tac [("x1","y")] (abs_ge_zero RS real_le_imp_less_or_eq) 1);
 by (EVERY1[etac disjE,rtac real_less_imp_le]);
 by (dres_inst_tac [("W","#1")]  real_less_sum_gt_zero 1);
-by (forw_inst_tac [("y","abs x + (-#1)")] (full_rename_numerals thy
-    real_mult_order) 1);
+by (forw_inst_tac [("y","abs x + (-#1)")] 
+    (rename_numerals thy real_mult_order) 1);
 by (rtac real_sum_gt_zero_less 2);
 by (asm_full_simp_tac (simpset() 
     addsimps [real_add_mult_distrib2,