# HG changeset patch
# User nipkow
# Date 977411920 -3600
# Node ID c09d4ebfec83e425e0b9d8dc5011a457336ef736
# Parent  01aec27d4c4549c142647d2461ebe1c83c54f594
rational arithemtic

diff -r 01aec27d4c45 -r c09d4ebfec83 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Thu Dec 21 10:40:08 2000 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Thu Dec 21 16:18:40 2000 +0100
@@ -340,8 +340,8 @@
         | mk(NotLeDD(j)) = trace_thm "NLeD" (hd([mk j RS LA_Logic.not_leD] RL lessD))
         | mk(NotLessD(j)) = trace_thm "NL" (mk j RS LA_Logic.not_lessD)
         | mk(Added(j1,j2)) = simp (trace_thm "+" (addthms (mk j1) (mk j2)))
-        | mk(Multiplied(n,j)) = (trace_msg "*"; multn(n,mk j))
-        | mk(Multiplied2(n,j)) = simp (trace_msg "*2"; multn2(n,mk j))
+        | mk(Multiplied(n,j)) = (trace_msg("*"^string_of_int n); trace_thm "*" (multn(n,mk j)))
+        | mk(Multiplied2(n,j)) = simp (trace_msg("**"^string_of_int n); trace_thm "**" (multn2(n,mk j)))
 
   in trace_msg "mkthm";
      simplify simpset (mk just) handle FalseE thm => thm end