# HG changeset patch
# User wenzelm
# Date 964476022 -7200
# Node ID 8b7aad2abcc9ef33b930cec382a76eec46c9d6ab
# Parent  f921cca1067d4613d1eff55661787e8433bdde71
avoid referencing thy value;
rename_numerals: use implicit theory context;

diff -r f921cca1067d -r 8b7aad2abcc9 src/HOL/Real/Hyperreal/HyperDef.ML
--- a/src/HOL/Real/Hyperreal/HyperDef.ML	Tue Jul 25 00:00:03 2000 +0200
+++ b/src/HOL/Real/Hyperreal/HyperDef.ML	Tue Jul 25 00:00:22 2000 +0200
@@ -171,7 +171,7 @@
 by (Fast_tac 1);
 qed "hyprelE_lemma";
 
-val [major,minor] = goal thy
+val [major,minor] = goal (the_context ())
   "[| p: hyprel;  \
 \     !!X Y. [| p = (X,Y); {n. X n = Y n}: FreeUltrafilterNat\
 \                    |] ==> Q |] ==> Q";
@@ -268,7 +268,7 @@
 by Auto_tac;
 qed "inj_hypreal_of_real";
 
-val [prem] = goal thy
+val [prem] = goal (the_context ())
     "(!!x y. z = Abs_hypreal(hyprel^^{x}) ==> P) ==> P";
 by (res_inst_tac [("x1","z")] 
     (rewrite_rule [hypreal_def] Rep_hypreal RS quotientE) 1);
@@ -340,8 +340,7 @@
 by (rotate_tac 1 1);
 by (asm_full_simp_tac (simpset() addsimps 
     [hypreal_hrinv,hypreal_zero_def] addsplits [split_if]) 1);
-by (ultra_tac (claset() addDs (map (rename_numerals thy)
-			       [rinv_not_zero,real_rinv_rinv]),
+by (ultra_tac (claset() addDs (map rename_numerals [rinv_not_zero,real_rinv_rinv]),
 	       simpset()) 1);
 qed "hypreal_hrinv_hrinv";
 
@@ -541,7 +540,7 @@
 by (asm_simp_tac (simpset() addsimps [hypreal_mult,real_mult_assoc]) 1);
 qed "hypreal_mult_assoc";
 
-qed_goal "hypreal_mult_left_commute" thy
+qed_goal "hypreal_mult_left_commute" (the_context ())
     "(z1::hypreal) * (z2 * z3) = z2 * (z1 * z3)"
  (fn _ => [rtac (hypreal_mult_commute RS trans) 1, rtac (hypreal_mult_assoc RS trans) 1,
            rtac (hypreal_mult_commute RS arg_cong) 1]);
@@ -702,7 +701,7 @@
     hypreal_mult] addsplits [split_if]) 1);
 by (dtac FreeUltrafilterNat_Compl_mem 1 THEN Clarify_tac 1);
 by (ultra_tac (claset() addIs [ccontr]
-                        addDs [rename_numerals thy rinv_not_zero],
+                        addDs [rename_numerals rinv_not_zero],
 	       simpset()) 1);
 qed "hrinv_not_zero";
 
@@ -847,7 +846,7 @@
 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
 by (auto_tac (claset() addSIs [exI],simpset() addsimps
     [hypreal_less_def,hypreal_mult]));
-by (ultra_tac (claset() addIs [rename_numerals thy real_mult_order],
+by (ultra_tac (claset() addIs [rename_numerals real_mult_order],
 	       simpset()) 1);
 qed "hypreal_mult_order";
 
@@ -1214,7 +1213,7 @@
 by (auto_tac (claset() addIs [hypreal_mult_le_less_mono2,hypreal_le_refl],simpset()));
 qed "hypreal_mult_le_le_mono1";
 
-val prem1::prem2::prem3::rest = goal thy
+val prem1::prem2::prem3::rest = goal (the_context ())
      "[| (0::hypreal)<y; x<r; y*r<t*s |] ==> y*x<t*s";
 by (rtac ([([prem1,prem2] MRS hypreal_mult_less_mono2),prem3] MRS hypreal_less_trans) 1);
 qed "hypreal_mult_less_trans";
@@ -1650,7 +1649,7 @@
 qed "hypreal_three_squares_add_zero_iff";
 Addsimps [hypreal_three_squares_add_zero_iff];
 
-Addsimps [rename_numerals thy real_le_square];
+Addsimps [rename_numerals real_le_square];
 Goal "(x::hypreal)*x <= x*x + y*y";
 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
@@ -1665,7 +1664,7 @@
 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
 by (auto_tac (claset(),
 	      simpset() addsimps [hypreal_mult, hypreal_add, hypreal_le,
-				  rename_numerals thy real_le_add_order]));
+				  rename_numerals real_le_add_order]));
 qed "hypreal_self_le_add_pos2";
 Addsimps [hypreal_self_le_add_pos2];
 
@@ -1682,7 +1681,7 @@
 Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 1 = 1hr + 1hr";
 by (full_simp_tac (simpset() addsimps 
 		   [real_of_preal_def,
-		    rename_numerals thy (real_one_def RS meta_eq_to_obj_eq),
+		    rename_numerals (real_one_def RS meta_eq_to_obj_eq),
 		    hypreal_add,hypreal_of_real_def,pnat_two_eq,
 		    hypreal_one_def, real_add,
 		    prat_of_pnat_add RS sym, preal_of_prat_add RS sym] @ 
@@ -1778,10 +1777,10 @@
 
 Goalw [epsilon_def,hypreal_zero_def] "ehr ~= 0";
 by (auto_tac (claset(),
-     simpset() addsimps [rename_numerals thy real_of_posnat_rinv_not_zero]));
+     simpset() addsimps [rename_numerals real_of_posnat_rinv_not_zero]));
 qed "hypreal_epsilon_not_zero";
 
-Addsimps [rename_numerals thy real_of_posnat_not_eq_zero];
+Addsimps [rename_numerals real_of_posnat_not_eq_zero];
 Goalw [omega_def,hypreal_zero_def] "whr ~= 0";
 by (Simp_tac 1);
 qed "hypreal_omega_not_zero";
diff -r f921cca1067d -r 8b7aad2abcc9 src/HOL/Real/RealAbs.ML
--- a/src/HOL/Real/RealAbs.ML	Tue Jul 25 00:00:03 2000 +0200
+++ b/src/HOL/Real/RealAbs.ML	Tue Jul 25 00:00:22 2000 +0200
@@ -13,7 +13,7 @@
 \       (if neg (number_of v) then number_of (bin_minus v) \
 \        else number_of v)";
 by (simp_tac
-    (simpset_of Int.thy addsimps
+    (simpset () addsimps
       bin_arith_simps@
       [minus_real_number_of, zero_eq_numeral_0, le_real_number_of_eq_not_less,
        less_real_number_of, real_of_int_le_iff]) 1);
@@ -26,7 +26,6 @@
 by(auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
 qed "abs_split";
 
-arith_tac_split_thms := !arith_tac_split_thms @ [abs_split];
 
 (*----------------------------------------------------------------------------
        Properties of the absolute value function over the reals
@@ -94,8 +93,8 @@
 Goalw [abs_real_def] "x~= (#0::real) ==> abs(rinv(x)) = rinv(abs(x))";
 by (auto_tac (claset(), 
               simpset() addsimps [real_le_less] @ 
-	    (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);
+	    (map rename_numerals [real_minus_rinv, real_rinv_gt_zero])));
+by (etac (rename_numerals (real_rinv_less_zero RSN (2,real_less_asym))) 1);
 by (arith_tac 1);
 qed "abs_rinv";
 
@@ -138,7 +137,7 @@
 qed "real_mult_0_less";
 
 Goal "[| (#0::real)<y; x<r; y*r<t*s |] ==> y*x<t*s";
-by (blast_tac (claset() addSIs [rename_numerals thy real_mult_less_mono2] 
+by (blast_tac (claset() addSIs [rename_numerals real_mult_less_mono2] 
                         addIs  [real_less_trans]) 1);
 qed "real_mult_less_trans";
 
@@ -153,7 +152,7 @@
 by (rtac real_mult_le_less_trans 1);
 by (rtac abs_ge_zero 1);
 by (assume_tac 1);
-by (rtac (rename_numerals thy real_mult_order) 2);
+by (rtac (rename_numerals 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,7 +167,7 @@
 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)")] 
-    (rename_numerals thy real_mult_order) 1);
+    (rename_numerals real_mult_order) 1);
 by (rtac real_sum_gt_zero_less 2);
 by (asm_full_simp_tac (simpset() 
     addsimps [real_add_mult_distrib2,
@@ -237,7 +236,7 @@
 
 Goal "abs (real_of_nat x) = real_of_nat x";
 by (auto_tac (claset() addIs [abs_eqI1],simpset()
-    addsimps [rename_numerals thy real_of_nat_ge_zero]));
+    addsimps [rename_numerals real_of_nat_ge_zero]));
 qed "abs_real_of_nat_cancel";
 Addsimps [abs_real_of_nat_cancel];