# HG changeset patch
# User webertj
# Date 1192219316 -7200
# Node ID 1a84a9ae9d58715118a6cca733523417575f76e3
# Parent  b711b0af178e89a2798f7d6d2ec7db5f88c4c8e6
typo in comment fixed

diff -r b711b0af178e -r 1a84a9ae9d58 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Fri Oct 12 22:00:47 2007 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Fri Oct 12 22:01:56 2007 +0200
@@ -187,7 +187,7 @@
          '1 / t' if the numerator can be reduced, but the denominator cannot. *)
       (* FIXME: Currently we even treat the whole fraction as atomic unless the
          denominator can be reduced to a numeric constant.  It might be better
-         to use the partially reduced denominator (i.e. 's / (2* t)' could be
+         to use the partially reduced denominator (i.e. 's / (2*t)' could be
          demult'ed to 's / t' with multiplicity .5).   This would require a
          very simple change only below, but it breaks existing proofs. *)
       (* quotient 's / t', where the denominator t can be NONE *)