# HG changeset patch
# User paulson
# Date 1072104085 -3600
# Node ID efda5615bb7d02e938261bd2a6d90d7c33b06b71
# Parent  1dd7439477dd9b900178a7eb0e3a1e961298dd30
new binding

diff -r 1dd7439477dd -r efda5615bb7d src/HOL/Complex/NSComplex.ML
--- 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];
diff -r 1dd7439477dd -r efda5615bb7d src/HOL/Real/real_arith.ML
--- 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";