--- a/src/HOL/Real/RealDef.ML Thu Sep 21 10:42:49 2000 +0200
+++ b/src/HOL/Real/RealDef.ML Thu Sep 21 12:11:38 2000 +0200
@@ -422,10 +422,6 @@
real_minus_mult_eq1 RS sym]) 1);
qed "real_minus_mult_commute";
-(*-----------------------------------------------------------------------------
-
- ----------------------------------------------------------------------------*)
-
(** Lemmas **)
Goal "(z::real) + v = z' + v' ==> z + (v + w) = z' + (v' + w)";
@@ -653,9 +649,6 @@
(* [| x < y; ~P ==> y < x |] ==> P *)
bind_thm ("real_less_asym", real_less_not_sym RS swap);
-(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)
- (****** Map and more real_less ******)
-(*** mapping from preal into real ***)
Goalw [real_of_preal_def]
"real_of_preal ((z1::preal) + z2) = \
\ real_of_preal z1 + real_of_preal z2";