src/HOL/Real/PRat.ML
changeset 9108 9fff97d29837
parent 9043 ca761fe227d8
child 9369 139fde7af7bd
     1.1 --- a/src/HOL/Real/PRat.ML	Thu Jun 22 11:37:13 2000 +0200
     1.2 +++ b/src/HOL/Real/PRat.ML	Thu Jun 22 23:04:34 2000 +0200
     1.3 @@ -59,7 +59,7 @@
     1.4                         addSEs [sym, prat_trans_lemma]) 1);
     1.5  qed "equiv_ratrel";
     1.6  
     1.7 -val equiv_ratrel_iff = [equiv_ratrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff;
     1.8 +bind_thm ("equiv_ratrel_iff", [equiv_ratrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff);
     1.9  
    1.10  Goalw  [prat_def,ratrel_def,quotient_def] "ratrel^^{(x,y)}:prat";
    1.11  by (Blast_tac 1);
    1.12 @@ -74,7 +74,7 @@
    1.13            ratrel_iff, ratrel_in_prat, Abs_prat_inverse];
    1.14  
    1.15  Addsimps [equiv_ratrel RS eq_equiv_class_iff];
    1.16 -val eq_ratrelD = equiv_ratrel RSN (2,eq_equiv_class);
    1.17 +bind_thm ("eq_ratrelD", equiv_ratrel RSN (2,eq_equiv_class));
    1.18  
    1.19  Goal "inj(Rep_prat)";
    1.20  by (rtac inj_inverseI 1);
    1.21 @@ -182,7 +182,7 @@
    1.22  qed "prat_add_left_commute";
    1.23  
    1.24  (* Positive Rational addition is an AC operator *)
    1.25 -val prat_add_ac = [prat_add_assoc, prat_add_commute, prat_add_left_commute];
    1.26 +bind_thms ("prat_add_ac", [prat_add_assoc, prat_add_commute, prat_add_left_commute]);
    1.27  
    1.28  
    1.29  (*** Congruence property for multiplication ***)
    1.30 @@ -228,8 +228,8 @@
    1.31  qed "prat_mult_left_commute";
    1.32  
    1.33  (*Positive Rational multiplication is an AC operator*)
    1.34 -val prat_mult_ac = [prat_mult_assoc,
    1.35 -                    prat_mult_commute,prat_mult_left_commute];
    1.36 +bind_thms ("prat_mult_ac", [prat_mult_assoc,
    1.37 +                    prat_mult_commute,prat_mult_left_commute]);
    1.38  
    1.39  Goalw [prat_of_pnat_def] 
    1.40        "(prat_of_pnat (Abs_pnat 1)) * z = z";
    1.41 @@ -572,7 +572,7 @@
    1.42  by (assume_tac 1);
    1.43  qed "prat_leD";
    1.44  
    1.45 -val prat_leE = make_elim prat_leD;
    1.46 +bind_thm ("prat_leE", make_elim prat_leD);
    1.47  
    1.48  Goal "(~(w < z)) = (z <= (w::prat))";
    1.49  by (fast_tac (claset() addSIs [prat_leI,prat_leD]) 1);