src/HOL/OrderedGroup.thy
changeset 22548 6ce4bddf3bcb
parent 22482 8fc3d7237e03
child 22986 d21d3539f6bb
     1.1 --- a/src/HOL/OrderedGroup.thy	Thu Mar 29 11:59:54 2007 +0200
     1.2 +++ b/src/HOL/OrderedGroup.thy	Thu Mar 29 14:21:45 2007 +0200
     1.3 @@ -1088,13 +1088,13 @@
     1.4     @{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel},
     1.5     @{thm minus_add_cancel}];
     1.6    
     1.7 -val eq_reflection = @{thm eq_reflection}
     1.8 +val eq_reflection = @{thm eq_reflection};
     1.9    
    1.10 -val thy_ref = Theory.self_ref @{theory}
    1.11 +val thy_ref = Theory.self_ref @{theory};
    1.12  
    1.13 -val T = TFree("'a", ["OrderedGroup.ab_group_add"])
    1.14 +val T = TFree("'a", ["OrderedGroup.ab_group_add"]);
    1.15  
    1.16 -val eqI_rules = [@{thm less_eqI}, @{thm le_eqI}, @{thm eq_eqI}]
    1.17 +val eqI_rules = [@{thm less_eqI}, @{thm le_eqI}, @{thm eq_eqI}];
    1.18  
    1.19  val dest_eqI = 
    1.20    fst o HOLogic.dest_bin "op =" HOLogic.boolT o HOLogic.dest_Trueprop o concl_of;
    1.21 @@ -1106,140 +1106,4 @@
    1.22    Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];
    1.23  *}
    1.24  
    1.25 -ML {*
    1.26 -val add_assoc = thm "add_assoc";
    1.27 -val add_commute = thm "add_commute";
    1.28 -val add_left_commute = thm "add_left_commute";
    1.29 -val add_ac = thms "add_ac";
    1.30 -val mult_assoc = thm "mult_assoc";
    1.31 -val mult_commute = thm "mult_commute";
    1.32 -val mult_left_commute = thm "mult_left_commute";
    1.33 -val mult_ac = thms "mult_ac";
    1.34 -val add_0 = thm "add_0";
    1.35 -val mult_1_left = thm "mult_1_left";
    1.36 -val mult_1_right = thm "mult_1_right";
    1.37 -val mult_1 = thm "mult_1";
    1.38 -val add_left_imp_eq = thm "add_left_imp_eq";
    1.39 -val add_right_imp_eq = thm "add_right_imp_eq";
    1.40 -val add_imp_eq = thm "add_imp_eq";
    1.41 -val left_minus = thm "left_minus";
    1.42 -val diff_minus = thm "diff_minus";
    1.43 -val add_0_right = thm "add_0_right";
    1.44 -val add_left_cancel = thm "add_left_cancel";
    1.45 -val add_right_cancel = thm "add_right_cancel";
    1.46 -val right_minus = thm "right_minus";
    1.47 -val right_minus_eq = thm "right_minus_eq";
    1.48 -val minus_minus = thm "minus_minus";
    1.49 -val equals_zero_I = thm "equals_zero_I";
    1.50 -val minus_zero = thm "minus_zero";
    1.51 -val diff_self = thm "diff_self";
    1.52 -val diff_0 = thm "diff_0";
    1.53 -val diff_0_right = thm "diff_0_right";
    1.54 -val diff_minus_eq_add = thm "diff_minus_eq_add";
    1.55 -val neg_equal_iff_equal = thm "neg_equal_iff_equal";
    1.56 -val neg_equal_0_iff_equal = thm "neg_equal_0_iff_equal";
    1.57 -val neg_0_equal_iff_equal = thm "neg_0_equal_iff_equal";
    1.58 -val equation_minus_iff = thm "equation_minus_iff";
    1.59 -val minus_equation_iff = thm "minus_equation_iff";
    1.60 -val minus_add_distrib = thm "minus_add_distrib";
    1.61 -val minus_diff_eq = thm "minus_diff_eq";
    1.62 -val add_left_mono = thm "add_left_mono";
    1.63 -val add_le_imp_le_left = thm "add_le_imp_le_left";
    1.64 -val add_right_mono = thm "add_right_mono";
    1.65 -val add_mono = thm "add_mono";
    1.66 -val add_strict_left_mono = thm "add_strict_left_mono";
    1.67 -val add_strict_right_mono = thm "add_strict_right_mono";
    1.68 -val add_strict_mono = thm "add_strict_mono";
    1.69 -val add_less_le_mono = thm "add_less_le_mono";
    1.70 -val add_le_less_mono = thm "add_le_less_mono";
    1.71 -val add_less_imp_less_left = thm "add_less_imp_less_left";
    1.72 -val add_less_imp_less_right = thm "add_less_imp_less_right";
    1.73 -val add_less_cancel_left = thm "add_less_cancel_left";
    1.74 -val add_less_cancel_right = thm "add_less_cancel_right";
    1.75 -val add_le_cancel_left = thm "add_le_cancel_left";
    1.76 -val add_le_cancel_right = thm "add_le_cancel_right";
    1.77 -val add_le_imp_le_right = thm "add_le_imp_le_right";
    1.78 -val add_increasing = thm "add_increasing";
    1.79 -val le_imp_neg_le = thm "le_imp_neg_le";
    1.80 -val neg_le_iff_le = thm "neg_le_iff_le";
    1.81 -val neg_le_0_iff_le = thm "neg_le_0_iff_le";
    1.82 -val neg_0_le_iff_le = thm "neg_0_le_iff_le";
    1.83 -val neg_less_iff_less = thm "neg_less_iff_less";
    1.84 -val neg_less_0_iff_less = thm "neg_less_0_iff_less";
    1.85 -val neg_0_less_iff_less = thm "neg_0_less_iff_less";
    1.86 -val less_minus_iff = thm "less_minus_iff";
    1.87 -val minus_less_iff = thm "minus_less_iff";
    1.88 -val le_minus_iff = thm "le_minus_iff";
    1.89 -val minus_le_iff = thm "minus_le_iff";
    1.90 -val add_diff_eq = thm "add_diff_eq";
    1.91 -val diff_add_eq = thm "diff_add_eq";
    1.92 -val diff_eq_eq = thm "diff_eq_eq";
    1.93 -val eq_diff_eq = thm "eq_diff_eq";
    1.94 -val diff_diff_eq = thm "diff_diff_eq";
    1.95 -val diff_diff_eq2 = thm "diff_diff_eq2";
    1.96 -val diff_add_cancel = thm "diff_add_cancel";
    1.97 -val add_diff_cancel = thm "add_diff_cancel";
    1.98 -val less_iff_diff_less_0 = thm "less_iff_diff_less_0";
    1.99 -val diff_less_eq = thm "diff_less_eq";
   1.100 -val less_diff_eq = thm "less_diff_eq";
   1.101 -val diff_le_eq = thm "diff_le_eq";
   1.102 -val le_diff_eq = thm "le_diff_eq";
   1.103 -val compare_rls = thms "compare_rls";
   1.104 -val eq_iff_diff_eq_0 = thm "eq_iff_diff_eq_0";
   1.105 -val le_iff_diff_le_0 = thm "le_iff_diff_le_0";
   1.106 -val add_inf_distrib_left = thm "add_inf_distrib_left";
   1.107 -val add_sup_distrib_left = thm "add_sup_distrib_left";
   1.108 -val add_sup_distrib_right = thm "add_sup_distrib_right";
   1.109 -val add_inf_distrib_right = thm "add_inf_distrib_right";
   1.110 -val add_sup_inf_distribs = thms "add_sup_inf_distribs";
   1.111 -val sup_eq_neg_inf = thm "sup_eq_neg_inf";
   1.112 -val inf_eq_neg_sup = thm "inf_eq_neg_sup";
   1.113 -val add_eq_inf_sup = thm "add_eq_inf_sup";
   1.114 -val prts = thm "prts";
   1.115 -val zero_le_pprt = thm "zero_le_pprt";
   1.116 -val nprt_le_zero = thm "nprt_le_zero";
   1.117 -val le_eq_neg = thm "le_eq_neg";
   1.118 -val sup_0_imp_0 = thm "sup_0_imp_0";
   1.119 -val inf_0_imp_0 = thm "inf_0_imp_0";
   1.120 -val sup_0_eq_0 = thm "sup_0_eq_0";
   1.121 -val inf_0_eq_0 = thm "inf_0_eq_0";
   1.122 -val zero_le_double_add_iff_zero_le_single_add = thm "zero_le_double_add_iff_zero_le_single_add";
   1.123 -val double_add_le_zero_iff_single_add_le_zero = thm "double_add_le_zero_iff_single_add_le_zero";
   1.124 -val double_add_less_zero_iff_single_less_zero = thm "double_add_less_zero_iff_single_less_zero";
   1.125 -val abs_lattice = thm "abs_lattice";
   1.126 -val abs_zero = thm "abs_zero";
   1.127 -val abs_eq_0 = thm "abs_eq_0";
   1.128 -val abs_0_eq = thm "abs_0_eq";
   1.129 -val neg_inf_eq_sup = thm "neg_inf_eq_sup";
   1.130 -val neg_sup_eq_inf = thm "neg_sup_eq_inf";
   1.131 -val sup_eq_if = thm "sup_eq_if";
   1.132 -val abs_if_lattice = thm "abs_if_lattice";
   1.133 -val abs_ge_zero = thm "abs_ge_zero";
   1.134 -val abs_le_zero_iff = thm "abs_le_zero_iff";
   1.135 -val zero_less_abs_iff = thm "zero_less_abs_iff";
   1.136 -val abs_not_less_zero = thm "abs_not_less_zero";
   1.137 -val abs_ge_self = thm "abs_ge_self";
   1.138 -val abs_ge_minus_self = thm "abs_ge_minus_self";
   1.139 -val le_imp_join_eq = thm "sup_absorb2";
   1.140 -val ge_imp_join_eq = thm "sup_absorb1";
   1.141 -val le_imp_meet_eq = thm "inf_absorb1";
   1.142 -val ge_imp_meet_eq = thm "inf_absorb2";
   1.143 -val abs_prts = thm "abs_prts";
   1.144 -val abs_minus_cancel = thm "abs_minus_cancel";
   1.145 -val abs_idempotent = thm "abs_idempotent";
   1.146 -val zero_le_iff_zero_nprt = thm "zero_le_iff_zero_nprt";
   1.147 -val le_zero_iff_zero_pprt = thm "le_zero_iff_zero_pprt";
   1.148 -val le_zero_iff_pprt_id = thm "le_zero_iff_pprt_id";
   1.149 -val zero_le_iff_nprt_id = thm "zero_le_iff_nprt_id";
   1.150 -val iff2imp = thm "iff2imp";
   1.151 -val abs_leI = thm "abs_leI";
   1.152 -val le_minus_self_iff = thm "le_minus_self_iff";
   1.153 -val minus_le_self_iff = thm "minus_le_self_iff";
   1.154 -val abs_le_D1 = thm "abs_le_D1";
   1.155 -val abs_le_D2 = thm "abs_le_D2";
   1.156 -val abs_le_iff = thm "abs_le_iff";
   1.157 -val abs_triangle_ineq = thm "abs_triangle_ineq";
   1.158 -val abs_diff_triangle_ineq = thm "abs_diff_triangle_ineq";
   1.159 -*}
   1.160 -
   1.161  end