diff -r 697dcaaf478f -r 0fba0357c04c doc-src/TutorialI/Rules/rules.tex
--- a/doc-src/TutorialI/Rules/rules.tex	Wed Aug 08 14:33:10 2001 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex	Wed Aug 08 14:50:28 2001 +0200
@@ -1819,7 +1819,7 @@
 appearance from left to right.  In this case, the variables  are \isa{?k}, \isa{?m}
 and~\isa{?n}. So, the expression
 \hbox{\texttt{[of k 1]}} replaces \isa{?k} by~\isa{k} and \isa{?m}
-by~\isa{1}.
+by~\isa{1}.\REMARK{which 1 do we use?? (right the way down)}
 \begin{isabelle}
 \isacommand{lemmas}\ gcd_mult_0\ =\ gcd_mult_distrib2\ [of\ k\ 1]
 \end{isabelle}