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