src/HOL/Integ/int_arith1.ML
changeset 14329 ff3210fe968f
parent 14273 e33ffff0123c
child 14331 8dbbb7cf3637
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Wed Dec 24 08:54:30 2003 +0100
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Thu Dec 25 22:48:32 2003 +0100
     1.3 @@ -5,6 +5,43 @@
     1.4  Simprocs and decision procedure for linear arithmetic.
     1.5  *)
     1.6  
     1.7 +(** Misc ML bindings **)
     1.8 +
     1.9 +val left_inverse = thm "left_inverse";
    1.10 +val right_inverse = thm "right_inverse";
    1.11 +val inverse_less_iff_less = thm"Ring_and_Field.inverse_less_iff_less";
    1.12 +val inverse_eq_divide = thm"Ring_and_Field.inverse_eq_divide";
    1.13 +val inverse_minus_eq = thm "inverse_minus_eq";
    1.14 +val inverse_mult_distrib = thm "inverse_mult_distrib";
    1.15 +val inverse_add = thm "inverse_add";
    1.16 +val inverse_inverse_eq = thm "inverse_inverse_eq";
    1.17 +
    1.18 +val add_right_mono = thm"Ring_and_Field.add_right_mono";
    1.19 +val times_divide_eq_left = thm "times_divide_eq_left";
    1.20 +val times_divide_eq_right = thm "times_divide_eq_right";
    1.21 +val minus_minus = thm "minus_minus";
    1.22 +val minus_mult_left = thm "minus_mult_left";
    1.23 +val minus_mult_right = thm "minus_mult_right";
    1.24 +
    1.25 +val pos_real_less_divide_eq = thm"pos_less_divide_eq";
    1.26 +val pos_real_divide_less_eq = thm"pos_divide_less_eq";
    1.27 +val pos_real_le_divide_eq = thm"pos_le_divide_eq";
    1.28 +val pos_real_divide_le_eq = thm"pos_divide_le_eq";
    1.29 +
    1.30 +val mult_less_cancel_left = thm"Ring_and_Field.mult_less_cancel_left";
    1.31 +val mult_le_cancel_left = thm"Ring_and_Field.mult_le_cancel_left";
    1.32 +val mult_less_cancel_right = thm"Ring_and_Field.mult_less_cancel_right";
    1.33 +val mult_le_cancel_right = thm"Ring_and_Field.mult_le_cancel_right";
    1.34 +val mult_cancel_left = thm"Ring_and_Field.mult_cancel_left";
    1.35 +val mult_cancel_right = thm"Ring_and_Field.mult_cancel_right";
    1.36 +
    1.37 +val field_mult_cancel_left = thm "field_mult_cancel_left";
    1.38 +val field_mult_cancel_right = thm "field_mult_cancel_right";
    1.39 +
    1.40 +val mult_divide_cancel_left = thm"Ring_and_Field.mult_divide_cancel_left";
    1.41 +val mult_divide_cancel_right = thm "Ring_and_Field.mult_divide_cancel_right";
    1.42 +val mult_divide_cancel_eq_if = thm"Ring_and_Field.mult_divide_cancel_eq_if";
    1.43 +
    1.44  val NCons_Pls = thm"NCons_Pls";
    1.45  val NCons_Min = thm"NCons_Min";
    1.46  val NCons_BIT = thm"NCons_BIT";