src/HOL/Real/Hyperreal/Series.ML

 Goalw [real_diff_def] "x ~= y ==> x - y ~= (#0::real)";
 by (asm_full_simp_tac (simpset() addsimps 
    [rename_numerals (real_eq_minus_iff2 RS sym)]) 1);
 qed "real_not_eq_diff";
 
-Goal "x ~= #1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - #1) * rinv(x - #1)";
+Goal "x ~= #1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - #1) * inverse(x - #1)";
 by (induct_tac "n" 1);
 by (Auto_tac);
 by (res_inst_tac [("c1","x - #1")] (real_mult_right_cancel RS iffD1) 1);
 by (auto_tac (claset(),simpset() addsimps [real_not_eq_diff,
     real_eq_minus_iff2 RS sym,real_mult_assoc,real_add_mult_distrib]));
 by (asm_full_simp_tac (simpset() addsimps [real_add_mult_distrib2,
     real_diff_def,real_mult_commute]) 1);
 qed "sumr_geometric";
 
-Goal "abs(x) < #1 ==> (%n. x ^ n) sums rinv(#1 - x)";
+Goal "abs(x) < #1 ==> (%n. x ^ n) sums inverse(#1 - x)";
 by (case_tac "x = #1" 1);
 by (auto_tac (claset() addSDs [LIMSEQ_rabs_realpow_zero2],
     simpset() addsimps [sumr_geometric,abs_one,sums_def,
     real_diff_def,real_add_mult_distrib]));
 by (rtac (real_add_zero_left RS subst) 1);
 by (rtac (real_mult_0 RS subst) 1);
 by (rtac LIMSEQ_add 1 THEN rtac LIMSEQ_mult 1);
 by (dtac real_not_eq_diff 3);
 by (auto_tac (claset() addIs [LIMSEQ_const], simpset() addsimps 
-    [real_minus_rinv RS sym,real_diff_def,real_add_commute,
+    [real_minus_inverse RS sym,real_diff_def,real_add_commute,
      rename_numerals LIMSEQ_rabs_realpow_zero2]));
 qed "geometric_sums";
 
 (*-------------------------------------------------------------------
     Cauchy-type criterion for convergence of series (c.f. Harrison)

 by (dtac real_le_trans 1 THEN assume_tac 1);
 by (TRYALL(arith_tac));
 qed "rabs_ratiotest_lemma";
 
 (* lemmas *)
-Goal "#0 < r ==> (x * r ^ n) * rinv (r ^ n) = x";
+Goal "#0 < (r::real) ==> (x * r ^ n) * inverse (r ^ n) = x";
 by (auto_tac (claset(),simpset() addsimps 
     [real_mult_assoc,rename_numerals realpow_not_zero]));
-val lemma_rinv_realpow = result();
-
-Goal "[| c ~= #0; ALL n. N <= n --> abs(f(Suc n)) <= c*abs(f n) |] \
-\  ==> ALL n. N <= n --> abs(f(Suc n)) <= (c * c ^ n)* (rinv(c ^ n)*abs(f n))";
+val lemma_inverse_realpow = result();
+
+Goal "[| (c::real) ~= #0; ALL n. N <= n --> abs(f(Suc n)) <= c*abs(f n) |] \
+\  ==> ALL n. N <= n --> abs(f(Suc n)) <= (c * c ^ n)* (inverse(c ^ n)*abs(f n))";
 by (auto_tac (claset(),simpset() addsimps real_mult_ac));
 by (res_inst_tac [("z2.1","c ^ n")] (real_mult_left_commute RS subst) 1);
 by (auto_tac (claset(),simpset() addsimps [rename_numerals  
     realpow_not_zero]));
-val lemma_rinv_realpow2 = result();
+val lemma_inverse_realpow2 = result();
 
 Goal "(k::nat) <= l ==> (EX n. l = k + n)";
 by (dtac le_imp_less_or_eq 1);
 by (auto_tac (claset() addDs [less_imp_Suc_add], simpset()));
 qed "le_Suc_ex";

 by (asm_full_simp_tac (simpset() addsimps [summable_Cauchy]) 1);
 by (Step_tac 1 THEN subgoal_tac "ALL n. N <= n --> f (Suc n) = #0" 1);
 by (blast_tac (claset() addIs [rabs_ratiotest_lemma]) 2);
 by (res_inst_tac [("x","Suc N")] exI 1 THEN Step_tac 1);
 by (dtac Suc_le_imp_diff_ge2 1 THEN Auto_tac);
-by (res_inst_tac [("g","%n. (abs (f N)* rinv(c ^ N))*c ^ n")] 
+by (res_inst_tac [("g","%n. (abs (f N)* inverse(c ^ N))*c ^ n")] 
     summable_comparison_test 1);
 by (res_inst_tac [("x","N")] exI 1 THEN Step_tac 1);
 by (dtac (le_Suc_ex_iff RS iffD1) 1);
 by (auto_tac (claset(),simpset() addsimps [realpow_add,
     CLAIM_SIMP "(a * b) * (c * d) = (a * d) * (b * (c::real))" real_mult_ac,

 by (induct_tac "na" 1 THEN Auto_tac);
 by (res_inst_tac [("j","c*abs(f(N + n))")] real_le_trans 1);
 by (auto_tac (claset() addIs [real_mult_le_le_mono1],
     simpset() addsimps [summable_def, CLAIM_SIMP 
     "a * (b * c) = b * (a * (c::real))" real_mult_ac]));
-by (res_inst_tac [("x","(abs(f N)*rinv(c ^ N))*rinv(#1 - c)")] exI 1);
+by (res_inst_tac [("x","(abs(f N)*inverse(c ^ N))*inverse(#1 - c)")] exI 1);
 by (auto_tac (claset() addSIs [sums_mult,geometric_sums], simpset() addsimps 
     [abs_eqI2]));
 qed "ratio_test";