--- a/src/HOL/Integ/int_arith1.ML Thu Dec 25 23:18:04 2003 +0100
+++ b/src/HOL/Integ/int_arith1.ML Sat Dec 27 21:02:14 2003 +0100
@@ -7,41 +7,6 @@
(** Misc ML bindings **)
-val left_inverse = thm "left_inverse";
-val right_inverse = thm "right_inverse";
-val inverse_less_iff_less = thm"Ring_and_Field.inverse_less_iff_less";
-val inverse_eq_divide = thm"Ring_and_Field.inverse_eq_divide";
-val inverse_minus_eq = thm "inverse_minus_eq";
-val inverse_mult_distrib = thm "inverse_mult_distrib";
-val inverse_add = thm "inverse_add";
-val inverse_inverse_eq = thm "inverse_inverse_eq";
-
-val add_right_mono = thm"Ring_and_Field.add_right_mono";
-val times_divide_eq_left = thm "times_divide_eq_left";
-val times_divide_eq_right = thm "times_divide_eq_right";
-val minus_minus = thm "minus_minus";
-val minus_mult_left = thm "minus_mult_left";
-val minus_mult_right = thm "minus_mult_right";
-
-val pos_real_less_divide_eq = thm"pos_less_divide_eq";
-val pos_real_divide_less_eq = thm"pos_divide_less_eq";
-val pos_real_le_divide_eq = thm"pos_le_divide_eq";
-val pos_real_divide_le_eq = thm"pos_divide_le_eq";
-
-val mult_less_cancel_left = thm"Ring_and_Field.mult_less_cancel_left";
-val mult_le_cancel_left = thm"Ring_and_Field.mult_le_cancel_left";
-val mult_less_cancel_right = thm"Ring_and_Field.mult_less_cancel_right";
-val mult_le_cancel_right = thm"Ring_and_Field.mult_le_cancel_right";
-val mult_cancel_left = thm"Ring_and_Field.mult_cancel_left";
-val mult_cancel_right = thm"Ring_and_Field.mult_cancel_right";
-
-val field_mult_cancel_left = thm "field_mult_cancel_left";
-val field_mult_cancel_right = thm "field_mult_cancel_right";
-
-val mult_divide_cancel_left = thm"Ring_and_Field.mult_divide_cancel_left";
-val mult_divide_cancel_right = thm "Ring_and_Field.mult_divide_cancel_right";
-val mult_divide_cancel_eq_if = thm"Ring_and_Field.mult_divide_cancel_eq_if";
-
val NCons_Pls = thm"NCons_Pls";
val NCons_Min = thm"NCons_Min";
val NCons_BIT = thm"NCons_BIT";