| changeset 15055 | aed573241bea |
| parent 15013 | 34264f5e4691 |
| child 15131 | c69542757a4d |
--- a/src/HOL/Real/PReal.thy Fri Jul 16 17:31:54 2004 +0200 +++ b/src/HOL/Real/PReal.thy Fri Jul 16 17:32:34 2004 +0200 @@ -356,7 +356,7 @@ apply (force simp add: mult_commute) done -text{*Multiplication of two positive reals gives a positive real.} +text{*Multiplication of two positive reals gives a positive real.*} text{*Lemmas for proving positive reals multiplication set in @{typ preal}*}