--- a/src/HOL/Ring_and_Field.thy Thu Dec 25 23:18:04 2003 +0100
+++ b/src/HOL/Ring_and_Field.thy Sat Dec 27 21:02:14 2003 +0100
@@ -1503,5 +1503,240 @@
thus ?thesis by (simp add: ac cpos mult_strict_mono)
qed
+ML
+{*
+val add_0_right = thm"add_0_right";
+val add_left_commute = thm"add_left_commute";
+val right_minus = thm"right_minus";
+val right_minus_eq = thm"right_minus_eq";
+val add_left_cancel = thm"add_left_cancel";
+val add_right_cancel = thm"add_right_cancel";
+val minus_minus = thm"minus_minus";
+val equals_zero_I = thm"equals_zero_I";
+val minus_zero = thm"minus_zero";
+val diff_self = thm"diff_self";
+val diff_0 = thm"diff_0";
+val diff_0_right = thm"diff_0_right";
+val diff_minus_eq_add = thm"diff_minus_eq_add";
+val neg_equal_iff_equal = thm"neg_equal_iff_equal";
+val neg_equal_0_iff_equal = thm"neg_equal_0_iff_equal";
+val neg_0_equal_iff_equal = thm"neg_0_equal_iff_equal";
+val equation_minus_iff = thm"equation_minus_iff";
+val minus_equation_iff = thm"minus_equation_iff";
+val mult_1_right = thm"mult_1_right";
+val mult_left_commute = thm"mult_left_commute";
+val mult_left_zero = thm"mult_left_zero";
+val mult_right_zero = thm"mult_right_zero";
+val right_distrib = thm"right_distrib";
+val combine_common_factor = thm"combine_common_factor";
+val minus_add_distrib = thm"minus_add_distrib";
+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 right_diff_distrib = thm"right_diff_distrib";
+val left_diff_distrib = thm"left_diff_distrib";
+val minus_diff_eq = thm"minus_diff_eq";
+val add_right_mono = thm"add_right_mono";
+val add_mono = thm"add_mono";
+val add_strict_left_mono = thm"add_strict_left_mono";
+val add_strict_right_mono = thm"add_strict_right_mono";
+val add_strict_mono = thm"add_strict_mono";
+val add_less_imp_less_left = thm"add_less_imp_less_left";
+val add_less_imp_less_right = thm"add_less_imp_less_right";
+val add_less_cancel_left = thm"add_less_cancel_left";
+val add_less_cancel_right = thm"add_less_cancel_right";
+val add_le_cancel_left = thm"add_le_cancel_left";
+val add_le_cancel_right = thm"add_le_cancel_right";
+val add_le_imp_le_left = thm"add_le_imp_le_left";
+val add_le_imp_le_right = thm"add_le_imp_le_right";
+val le_imp_neg_le = thm"le_imp_neg_le";
+val neg_le_iff_le = thm"neg_le_iff_le";
+val neg_le_0_iff_le = thm"neg_le_0_iff_le";
+val neg_0_le_iff_le = thm"neg_0_le_iff_le";
+val neg_less_iff_less = thm"neg_less_iff_less";
+val neg_less_0_iff_less = thm"neg_less_0_iff_less";
+val neg_0_less_iff_less = thm"neg_0_less_iff_less";
+val less_minus_iff = thm"less_minus_iff";
+val minus_less_iff = thm"minus_less_iff";
+val le_minus_iff = thm"le_minus_iff";
+val minus_le_iff = thm"minus_le_iff";
+val add_diff_eq = thm"add_diff_eq";
+val diff_add_eq = thm"diff_add_eq";
+val diff_eq_eq = thm"diff_eq_eq";
+val eq_diff_eq = thm"eq_diff_eq";
+val diff_diff_eq = thm"diff_diff_eq";
+val diff_diff_eq2 = thm"diff_diff_eq2";
+val less_iff_diff_less_0 = thm"less_iff_diff_less_0";
+val diff_less_eq = thm"diff_less_eq";
+val less_diff_eq = thm"less_diff_eq";
+val diff_le_eq = thm"diff_le_eq";
+val le_diff_eq = thm"le_diff_eq";
+val eq_iff_diff_eq_0 = thm"eq_iff_diff_eq_0";
+val le_iff_diff_le_0 = thm"le_iff_diff_le_0";
+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_strict_right_mono = thm"mult_strict_right_mono";
+val mult_left_mono = thm"mult_left_mono";
+val mult_right_mono = thm"mult_right_mono";
+val mult_strict_left_mono_neg = thm"mult_strict_left_mono_neg";
+val mult_strict_right_mono_neg = thm"mult_strict_right_mono_neg";
+val mult_pos = thm"mult_pos";
+val mult_pos_neg = thm"mult_pos_neg";
+val mult_neg = thm"mult_neg";
+val zero_less_mult_pos = thm"zero_less_mult_pos";
+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 zero_le_square = thm"zero_le_square";
+val zero_less_one = thm"zero_less_one";
+val zero_le_one = thm"zero_le_one";
+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 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 left_inverse = thm "left_inverse";
+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_inverse_zero = thm"divide_inverse_zero";
+val divide_zero_left = thm"divide_zero_left";
+val inverse_eq_divide = thm"inverse_eq_divide";
+val nonzero_add_divide_distrib = thm"nonzero_add_divide_distrib";
+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 = 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 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 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 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_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 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_zero = thm"abs_zero";
+val abs_one = thm"abs_one";
+val abs_mult = thm"abs_mult";
+val abs_eq_0 = thm"abs_eq_0";
+val zero_less_abs_iff = thm"zero_less_abs_iff";
+val abs_not_less_zero = thm"abs_not_less_zero";
+val abs_le_zero_iff = thm"abs_le_zero_iff";
+val abs_minus_cancel = thm"abs_minus_cancel";
+val abs_ge_zero = thm"abs_ge_zero";
+val abs_idempotent = thm"abs_idempotent";
+val abs_zero_iff = thm"abs_zero_iff";
+val abs_ge_self = thm"abs_ge_self";
+val abs_ge_minus_self = thm"abs_ge_minus_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_leI = thm"abs_leI";
+val le_minus_self_iff = thm"le_minus_self_iff";
+val minus_le_self_iff = thm"minus_le_self_iff";
+val eq_minus_self_iff = thm"eq_minus_self_iff";
+val less_minus_self_iff = thm"less_minus_self_iff";
+val abs_le_D1 = thm"abs_le_D1";
+val abs_le_D2 = thm"abs_le_D2";
+val abs_le_iff = thm"abs_le_iff";
+val abs_less_iff = thm"abs_less_iff";
+val abs_triangle_ineq = thm"abs_triangle_ineq";
+val abs_mult_less = thm"abs_mult_less";
+
+val compare_rls = thms"compare_rls";
+*}
+
end