--- a/src/HOL/Integ/int_arith1.ML Wed Dec 24 08:54:30 2003 +0100
+++ b/src/HOL/Integ/int_arith1.ML Thu Dec 25 22:48:32 2003 +0100
@@ -5,6 +5,43 @@
Simprocs and decision procedure for linear arithmetic.
*)
+(** 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";