src/HOL/Real/RealDef.ML
changeset 10043 a0364652e115
parent 9969 4753185f1dd2
child 10232 529c65b5dcde
     1.1 --- a/src/HOL/Real/RealDef.ML	Thu Sep 21 10:42:49 2000 +0200
     1.2 +++ b/src/HOL/Real/RealDef.ML	Thu Sep 21 12:11:38 2000 +0200
     1.3 @@ -422,10 +422,6 @@
     1.4  				       real_minus_mult_eq1 RS sym]) 1);
     1.5  qed "real_minus_mult_commute";
     1.6  
     1.7 -(*-----------------------------------------------------------------------------
     1.8 -
     1.9 - ----------------------------------------------------------------------------*)
    1.10 -
    1.11  (** Lemmas **)
    1.12  
    1.13  Goal "(z::real) + v = z' + v' ==> z + (v + w) = z' + (v' + w)";
    1.14 @@ -653,9 +649,6 @@
    1.15  (* [| x < y;  ~P ==> y < x |] ==> P *)
    1.16  bind_thm ("real_less_asym", real_less_not_sym RS swap);
    1.17  
    1.18 -(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)
    1.19 -    (****** Map and more real_less ******)
    1.20 -(*** mapping from preal into real ***)
    1.21  Goalw [real_of_preal_def] 
    1.22       "real_of_preal ((z1::preal) + z2) = \
    1.23  \     real_of_preal z1 + real_of_preal z2";