src/HOL/Real/PReal.ML
changeset 9108 9fff97d29837
parent 9043 ca761fe227d8
child 9189 69b71b554e91
     1.1 --- a/src/HOL/Real/PReal.ML	Thu Jun 22 11:37:13 2000 +0200
     1.2 +++ b/src/HOL/Real/PReal.ML	Thu Jun 22 23:04:34 2000 +0200
     1.3 @@ -281,7 +281,7 @@
     1.4             rtac (preal_add_commute RS arg_cong) 1]);
     1.5  
     1.6  (* Positive Reals addition is an AC operator *)
     1.7 -val preal_add_ac = [preal_add_assoc, preal_add_commute, preal_add_left_commute];
     1.8 +bind_thms ("preal_add_ac", [preal_add_assoc, preal_add_commute, preal_add_left_commute]);
     1.9  
    1.10    (*** Properties of multiplication ***)
    1.11  
    1.12 @@ -367,9 +367,9 @@
    1.13             rtac (preal_mult_commute RS arg_cong) 1]);
    1.14  
    1.15  (* Positive Reals multiplication is an AC operator *)
    1.16 -val preal_mult_ac = [preal_mult_assoc, 
    1.17 +bind_thms ("preal_mult_ac", [preal_mult_assoc, 
    1.18                       preal_mult_commute, 
    1.19 -                     preal_mult_left_commute];
    1.20 +                     preal_mult_left_commute]);
    1.21  
    1.22  (* Positive Real 1 is the multiplicative identity element *) 
    1.23  (* long *)
    1.24 @@ -746,7 +746,7 @@
    1.25  by (auto_tac  (claset() addDs [equalityI],simpset()));
    1.26  qed "preal_leD";
    1.27  
    1.28 -val preal_leE = make_elim preal_leD;
    1.29 +bind_thm ("preal_leE", make_elim preal_leD);
    1.30  
    1.31  Goalw [preal_le_def,psubset_def,preal_less_def]
    1.32                     "~ z <= w ==> w<(z::preal)";