src/HOL/Integ/int_arith1.ML
changeset 14331 8dbbb7cf3637
parent 14329 ff3210fe968f
child 14368 2763da611ad9
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Thu Dec 25 23:18:04 2003 +0100
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Sat Dec 27 21:02:14 2003 +0100
     1.3 @@ -7,41 +7,6 @@
     1.4  
     1.5  (** Misc ML bindings **)
     1.6  
     1.7 -val left_inverse = thm "left_inverse";
     1.8 -val right_inverse = thm "right_inverse";
     1.9 -val inverse_less_iff_less = thm"Ring_and_Field.inverse_less_iff_less";
    1.10 -val inverse_eq_divide = thm"Ring_and_Field.inverse_eq_divide";
    1.11 -val inverse_minus_eq = thm "inverse_minus_eq";
    1.12 -val inverse_mult_distrib = thm "inverse_mult_distrib";
    1.13 -val inverse_add = thm "inverse_add";
    1.14 -val inverse_inverse_eq = thm "inverse_inverse_eq";
    1.15 -
    1.16 -val add_right_mono = thm"Ring_and_Field.add_right_mono";
    1.17 -val times_divide_eq_left = thm "times_divide_eq_left";
    1.18 -val times_divide_eq_right = thm "times_divide_eq_right";
    1.19 -val minus_minus = thm "minus_minus";
    1.20 -val minus_mult_left = thm "minus_mult_left";
    1.21 -val minus_mult_right = thm "minus_mult_right";
    1.22 -
    1.23 -val pos_real_less_divide_eq = thm"pos_less_divide_eq";
    1.24 -val pos_real_divide_less_eq = thm"pos_divide_less_eq";
    1.25 -val pos_real_le_divide_eq = thm"pos_le_divide_eq";
    1.26 -val pos_real_divide_le_eq = thm"pos_divide_le_eq";
    1.27 -
    1.28 -val mult_less_cancel_left = thm"Ring_and_Field.mult_less_cancel_left";
    1.29 -val mult_le_cancel_left = thm"Ring_and_Field.mult_le_cancel_left";
    1.30 -val mult_less_cancel_right = thm"Ring_and_Field.mult_less_cancel_right";
    1.31 -val mult_le_cancel_right = thm"Ring_and_Field.mult_le_cancel_right";
    1.32 -val mult_cancel_left = thm"Ring_and_Field.mult_cancel_left";
    1.33 -val mult_cancel_right = thm"Ring_and_Field.mult_cancel_right";
    1.34 -
    1.35 -val field_mult_cancel_left = thm "field_mult_cancel_left";
    1.36 -val field_mult_cancel_right = thm "field_mult_cancel_right";
    1.37 -
    1.38 -val mult_divide_cancel_left = thm"Ring_and_Field.mult_divide_cancel_left";
    1.39 -val mult_divide_cancel_right = thm "Ring_and_Field.mult_divide_cancel_right";
    1.40 -val mult_divide_cancel_eq_if = thm"Ring_and_Field.mult_divide_cancel_eq_if";
    1.41 -
    1.42  val NCons_Pls = thm"NCons_Pls";
    1.43  val NCons_Min = thm"NCons_Min";
    1.44  val NCons_BIT = thm"NCons_BIT";