# HG changeset patch
# User nipkow
# Date 1089991954 -7200
# Node ID aed573241bea2a34e29deb18645f27fc3fbddeee
# Parent  1ad0b310bc54d28ab44b6f61841045803afa15ce
Corrected TeX problem.

diff -r 1ad0b310bc54 -r aed573241bea src/HOL/Real/PReal.thy
--- 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}*}