Corrected TeX problem.

--- 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}*}