--- a/src/HOL/Complex/NSComplex.ML Mon Dec 22 14:12:54 2003 +0100
+++ b/src/HOL/Complex/NSComplex.ML Mon Dec 22 15:41:25 2003 +0100
@@ -1067,8 +1067,8 @@
Addsimps [hcmod_triangle_ineq];
Goal "hcmod(b + a) - hcmod b <= hcmod a";
-by (cut_inst_tac [("x1","b"),("y1","a"),("x","-hcmod b")]
- (hcmod_triangle_ineq RS hypreal_add_le_mono1) 1);
+by (cut_inst_tac [("x1","b"),("y1","a"),("c","-hcmod b")]
+ (hcmod_triangle_ineq RS add_right_mono) 1);
by (asm_full_simp_tac (simpset() addsimps hypreal_add_ac) 1);
qed "hcmod_triangle_ineq2";
Addsimps [hcmod_triangle_ineq2];
--- a/src/HOL/Real/real_arith.ML Mon Dec 22 14:12:54 2003 +0100
+++ b/src/HOL/Real/real_arith.ML Mon Dec 22 15:41:25 2003 +0100
@@ -9,7 +9,8 @@
(** Misc ML bindings **)
-val inverse_less_iff_less = thm"inverse_less_iff_less";
+val inverse_less_iff_less = thm"Ring_and_Field.inverse_less_iff_less";
+val add_right_mono = thm"Ring_and_Field.add_right_mono";
val pos_real_less_divide_eq = thm"pos_less_divide_eq";
val pos_real_divide_less_eq = thm"pos_divide_less_eq";