src/HOL/Real/RealDef.ML
changeset 9108 9fff97d29837
parent 9043 ca761fe227d8
child 9167 5b6b65c90eeb
     1.1 --- a/src/HOL/Real/RealDef.ML	Thu Jun 22 11:37:13 2000 +0200
     1.2 +++ b/src/HOL/Real/RealDef.ML	Thu Jun 22 23:04:34 2000 +0200
     1.3 @@ -56,10 +56,10 @@
     1.4                        addSEs [sym,preal_trans_lemma]) 1);
     1.5  qed "equiv_realrel";
     1.6  
     1.7 -val equiv_realrel_iff =
     1.8 +bind_thm ("equiv_realrel_iff",
     1.9      [TrueI, TrueI] MRS 
    1.10      ([CollectI, CollectI] MRS 
    1.11 -    (equiv_realrel RS eq_equiv_class_iff));
    1.12 +    (equiv_realrel RS eq_equiv_class_iff)));
    1.13  
    1.14  Goalw  [real_def,realrel_def,quotient_def] "realrel^^{(x,y)}:real";
    1.15  by (Blast_tac 1);
    1.16 @@ -74,7 +74,7 @@
    1.17            realrel_iff, realrel_in_real, Abs_real_inverse];
    1.18  
    1.19  Addsimps [equiv_realrel RS eq_equiv_class_iff];
    1.20 -val eq_realrelD = equiv_realrel RSN (2,eq_equiv_class);
    1.21 +bind_thm ("eq_realrelD", equiv_realrel RSN (2,eq_equiv_class));
    1.22  
    1.23  Goal "inj(Rep_real)";
    1.24  by (rtac inj_inverseI 1);
    1.25 @@ -1081,11 +1081,11 @@
    1.26  (*This list of rewrites simplifies (in)equalities by bringing subtractions
    1.27    to the top and then moving negative terms to the other side.  
    1.28    Use with real_add_ac*)
    1.29 -val real_compare_rls = 
    1.30 +bind_thms ("real_compare_rls",
    1.31    [symmetric real_diff_def,
    1.32     real_add_diff_eq, real_diff_add_eq, real_diff_diff_eq, real_diff_diff_eq2, 
    1.33     real_diff_less_eq, real_less_diff_eq, real_diff_le_eq, real_le_diff_eq, 
    1.34 -   real_diff_eq_eq, real_eq_diff_eq];
    1.35 +   real_diff_eq_eq, real_eq_diff_eq]);
    1.36  
    1.37  
    1.38  (** For the cancellation simproc.