--- a/src/HOL/Ring_and_Field.thy Thu Mar 29 11:59:54 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy Thu Mar 29 14:21:45 2007 +0200
@@ -2067,210 +2067,4 @@
then show ?thesis by simp
qed
-ML {*
-val left_distrib = thm "left_distrib";
-val right_distrib = thm "right_distrib";
-val mult_commute = thm "mult_commute";
-val distrib = thm "distrib";
-val zero_neq_one = thm "zero_neq_one";
-val no_zero_divisors = thm "no_zero_divisors";
-val left_inverse = thm "left_inverse";
-val divide_inverse = thm "divide_inverse";
-val mult_zero_left = thm "mult_zero_left";
-val mult_zero_right = thm "mult_zero_right";
-val field_mult_eq_0_iff = thm "field_mult_eq_0_iff";
-val inverse_zero = thm "inverse_zero";
-val ring_distrib = thms "ring_distrib";
-val combine_common_factor = thm "combine_common_factor";
-val minus_mult_left = thm "minus_mult_left";
-val minus_mult_right = thm "minus_mult_right";
-val minus_mult_minus = thm "minus_mult_minus";
-val minus_mult_commute = thm "minus_mult_commute";
-val right_diff_distrib = thm "right_diff_distrib";
-val left_diff_distrib = thm "left_diff_distrib";
-val mult_left_mono = thm "mult_left_mono";
-val mult_right_mono = thm "mult_right_mono";
-val mult_strict_left_mono = thm "mult_strict_left_mono";
-val mult_strict_right_mono = thm "mult_strict_right_mono";
-val mult_mono = thm "mult_mono";
-val mult_strict_mono = thm "mult_strict_mono";
-val abs_if = thm "abs_if";
-val zero_less_one = thm "zero_less_one";
-val eq_add_iff1 = thm "eq_add_iff1";
-val eq_add_iff2 = thm "eq_add_iff2";
-val less_add_iff1 = thm "less_add_iff1";
-val less_add_iff2 = thm "less_add_iff2";
-val le_add_iff1 = thm "le_add_iff1";
-val le_add_iff2 = thm "le_add_iff2";
-val mult_left_le_imp_le = thm "mult_left_le_imp_le";
-val mult_right_le_imp_le = thm "mult_right_le_imp_le";
-val mult_left_less_imp_less = thm "mult_left_less_imp_less";
-val mult_right_less_imp_less = thm "mult_right_less_imp_less";
-val mult_strict_left_mono_neg = thm "mult_strict_left_mono_neg";
-val mult_left_mono_neg = thm "mult_left_mono_neg";
-val mult_strict_right_mono_neg = thm "mult_strict_right_mono_neg";
-val mult_right_mono_neg = thm "mult_right_mono_neg";
-(*
-val mult_pos = thm "mult_pos";
-val mult_pos_le = thm "mult_pos_le";
-val mult_pos_neg = thm "mult_pos_neg";
-val mult_pos_neg_le = thm "mult_pos_neg_le";
-val mult_pos_neg2 = thm "mult_pos_neg2";
-val mult_pos_neg2_le = thm "mult_pos_neg2_le";
-val mult_neg = thm "mult_neg";
-val mult_neg_le = thm "mult_neg_le";
-*)
-val zero_less_mult_pos = thm "zero_less_mult_pos";
-val zero_less_mult_pos2 = thm "zero_less_mult_pos2";
-val zero_less_mult_iff = thm "zero_less_mult_iff";
-val mult_eq_0_iff = thm "mult_eq_0_iff";
-val zero_le_mult_iff = thm "zero_le_mult_iff";
-val mult_less_0_iff = thm "mult_less_0_iff";
-val mult_le_0_iff = thm "mult_le_0_iff";
-val split_mult_pos_le = thm "split_mult_pos_le";
-val split_mult_neg_le = thm "split_mult_neg_le";
-val zero_le_square = thm "zero_le_square";
-val zero_le_one = thm "zero_le_one";
-val not_one_le_zero = thm "not_one_le_zero";
-val not_one_less_zero = thm "not_one_less_zero";
-val mult_left_mono_neg = thm "mult_left_mono_neg";
-val mult_right_mono_neg = thm "mult_right_mono_neg";
-val mult_strict_mono = thm "mult_strict_mono";
-val mult_strict_mono' = thm "mult_strict_mono'";
-val mult_mono = thm "mult_mono";
-val less_1_mult = thm "less_1_mult";
-val mult_less_cancel_right_disj = thm "mult_less_cancel_right_disj";
-val mult_less_cancel_left_disj = thm "mult_less_cancel_left_disj";
-val mult_less_cancel_right = thm "mult_less_cancel_right";
-val mult_less_cancel_left = thm "mult_less_cancel_left";
-val mult_le_cancel_right = thm "mult_le_cancel_right";
-val mult_le_cancel_left = thm "mult_le_cancel_left";
-val mult_less_imp_less_left = thm "mult_less_imp_less_left";
-val mult_less_imp_less_right = thm "mult_less_imp_less_right";
-val mult_cancel_right = thm "mult_cancel_right";
-val mult_cancel_left = thm "mult_cancel_left";
-val ring_eq_simps = thms "ring_eq_simps";
-val right_inverse = thm "right_inverse";
-val right_inverse_eq = thm "right_inverse_eq";
-val nonzero_inverse_eq_divide = thm "nonzero_inverse_eq_divide";
-val divide_self = thm "divide_self";
-val divide_zero = thm "divide_zero";
-val divide_zero_left = thm "divide_zero_left";
-val inverse_eq_divide = thm "inverse_eq_divide";
-val add_divide_distrib = thm "add_divide_distrib";
-val field_mult_eq_0_iff = thm "field_mult_eq_0_iff";
-val field_mult_cancel_right_lemma = thm "field_mult_cancel_right_lemma";
-val field_mult_cancel_right = thm "field_mult_cancel_right";
-val field_mult_cancel_left = thm "field_mult_cancel_left";
-val nonzero_imp_inverse_nonzero = thm "nonzero_imp_inverse_nonzero";
-val inverse_zero_imp_zero = thm "inverse_zero_imp_zero";
-val inverse_nonzero_imp_nonzero = thm "inverse_nonzero_imp_nonzero";
-val inverse_nonzero_iff_nonzero = thm "inverse_nonzero_iff_nonzero";
-val nonzero_inverse_minus_eq = thm "nonzero_inverse_minus_eq";
-val inverse_minus_eq = thm "inverse_minus_eq";
-val nonzero_inverse_eq_imp_eq = thm "nonzero_inverse_eq_imp_eq";
-val inverse_eq_imp_eq = thm "inverse_eq_imp_eq";
-val inverse_eq_iff_eq = thm "inverse_eq_iff_eq";
-val nonzero_inverse_inverse_eq = thm "nonzero_inverse_inverse_eq";
-val inverse_inverse_eq = thm "inverse_inverse_eq";
-val inverse_1 = thm "inverse_1";
-val nonzero_inverse_mult_distrib = thm "nonzero_inverse_mult_distrib";
-val inverse_mult_distrib = thm "inverse_mult_distrib";
-val inverse_add = thm "inverse_add";
-val inverse_divide = thm "inverse_divide";
-val nonzero_mult_divide_cancel_left = thm "nonzero_mult_divide_cancel_left";
-val mult_divide_cancel_left = thm "mult_divide_cancel_left";
-val nonzero_mult_divide_cancel_right = thm "nonzero_mult_divide_cancel_right";
-val mult_divide_cancel_right = thm "mult_divide_cancel_right";
-val mult_divide_cancel_eq_if = thm "mult_divide_cancel_eq_if";
-val divide_1 = thm "divide_1";
-val times_divide_eq_right = thm "times_divide_eq_right";
-val times_divide_eq_left = thm "times_divide_eq_left";
-val divide_divide_eq_right = thm "divide_divide_eq_right";
-val divide_divide_eq_left = thm "divide_divide_eq_left";
-val nonzero_minus_divide_left = thm "nonzero_minus_divide_left";
-val nonzero_minus_divide_right = thm "nonzero_minus_divide_right";
-val nonzero_minus_divide_divide = thm "nonzero_minus_divide_divide";
-val minus_divide_left = thm "minus_divide_left";
-val minus_divide_right = thm "minus_divide_right";
-val minus_divide_divide = thm "minus_divide_divide";
-val diff_divide_distrib = thm "diff_divide_distrib";
-val positive_imp_inverse_positive = thm "positive_imp_inverse_positive";
-val negative_imp_inverse_negative = thm "negative_imp_inverse_negative";
-val inverse_le_imp_le = thm "inverse_le_imp_le";
-val inverse_positive_imp_positive = thm "inverse_positive_imp_positive";
-val inverse_positive_iff_positive = thm "inverse_positive_iff_positive";
-val inverse_negative_imp_negative = thm "inverse_negative_imp_negative";
-val inverse_negative_iff_negative = thm "inverse_negative_iff_negative";
-val inverse_nonnegative_iff_nonnegative = thm "inverse_nonnegative_iff_nonnegative";
-val inverse_nonpositive_iff_nonpositive = thm "inverse_nonpositive_iff_nonpositive";
-val less_imp_inverse_less = thm "less_imp_inverse_less";
-val inverse_less_imp_less = thm "inverse_less_imp_less";
-val inverse_less_iff_less = thm "inverse_less_iff_less";
-val le_imp_inverse_le = thm "le_imp_inverse_le";
-val inverse_le_iff_le = thm "inverse_le_iff_le";
-val inverse_le_imp_le_neg = thm "inverse_le_imp_le_neg";
-val less_imp_inverse_less_neg = thm "less_imp_inverse_less_neg";
-val inverse_less_imp_less_neg = thm "inverse_less_imp_less_neg";
-val inverse_less_iff_less_neg = thm "inverse_less_iff_less_neg";
-val le_imp_inverse_le_neg = thm "le_imp_inverse_le_neg";
-val inverse_le_iff_le_neg = thm "inverse_le_iff_le_neg";
-val one_less_inverse_iff = thm "one_less_inverse_iff";
-val inverse_eq_1_iff = thm "inverse_eq_1_iff";
-val one_le_inverse_iff = thm "one_le_inverse_iff";
-val inverse_less_1_iff = thm "inverse_less_1_iff";
-val inverse_le_1_iff = thm "inverse_le_1_iff";
-val zero_less_divide_iff = thm "zero_less_divide_iff";
-val divide_less_0_iff = thm "divide_less_0_iff";
-val zero_le_divide_iff = thm "zero_le_divide_iff";
-val divide_le_0_iff = thm "divide_le_0_iff";
-val divide_eq_0_iff = thm "divide_eq_0_iff";
-val pos_le_divide_eq = thm "pos_le_divide_eq";
-val neg_le_divide_eq = thm "neg_le_divide_eq";
-val le_divide_eq = thm "le_divide_eq";
-val pos_divide_le_eq = thm "pos_divide_le_eq";
-val neg_divide_le_eq = thm "neg_divide_le_eq";
-val divide_le_eq = thm "divide_le_eq";
-val pos_less_divide_eq = thm "pos_less_divide_eq";
-val neg_less_divide_eq = thm "neg_less_divide_eq";
-val less_divide_eq = thm "less_divide_eq";
-val pos_divide_less_eq = thm "pos_divide_less_eq";
-val neg_divide_less_eq = thm "neg_divide_less_eq";
-val divide_less_eq = thm "divide_less_eq";
-val nonzero_eq_divide_eq = thm "nonzero_eq_divide_eq";
-val eq_divide_eq = thm "eq_divide_eq";
-val nonzero_divide_eq_eq = thm "nonzero_divide_eq_eq";
-val divide_eq_eq = thm "divide_eq_eq";
-val divide_cancel_right = thm "divide_cancel_right";
-val divide_cancel_left = thm "divide_cancel_left";
-val divide_eq_1_iff = thm "divide_eq_1_iff";
-val one_eq_divide_iff = thm "one_eq_divide_iff";
-val zero_eq_1_divide_iff = thm "zero_eq_1_divide_iff";
-val one_divide_eq_0_iff = thm "one_divide_eq_0_iff";
-val divide_strict_right_mono = thm "divide_strict_right_mono";
-val divide_right_mono = thm "divide_right_mono";
-val divide_strict_left_mono = thm "divide_strict_left_mono";
-val divide_left_mono = thm "divide_left_mono";
-val divide_strict_left_mono_neg = thm "divide_strict_left_mono_neg";
-val divide_strict_right_mono_neg = thm "divide_strict_right_mono_neg";
-val less_add_one = thm "less_add_one";
-val zero_less_two = thm "zero_less_two";
-val less_half_sum = thm "less_half_sum";
-val gt_half_sum = thm "gt_half_sum";
-val dense = thm "dense";
-val abs_one = thm "abs_one";
-val abs_le_mult = thm "abs_le_mult";
-val abs_eq_mult = thm "abs_eq_mult";
-val abs_mult = thm "abs_mult";
-val abs_mult_self = thm "abs_mult_self";
-val nonzero_abs_inverse = thm "nonzero_abs_inverse";
-val abs_inverse = thm "abs_inverse";
-val nonzero_abs_divide = thm "nonzero_abs_divide";
-val abs_divide = thm "abs_divide";
-val abs_mult_less = thm "abs_mult_less";
-val eq_minus_self_iff = thm "eq_minus_self_iff";
-val less_minus_self_iff = thm "less_minus_self_iff";
-val abs_less_iff = thm "abs_less_iff";
-*}
-
end