]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/papers/calculemus-2003/hbugs-calculemus-2003.tex
...
[helm.git] / helm / papers / calculemus-2003 / hbugs-calculemus-2003.tex
index 22036320c318cc0a0117ca56dc0db0936f8c8ca2..945740cf8adf06ca203469f0a5fc5a216994de6a 100644 (file)
@@ -247,8 +247,8 @@ x = \frac{(x+1)*(x+1) - 1 - x*x}{2}
 \end{displaymath}
 \end{exercise}
 
-\myincludegraphics{step1}{t}{12cm}{Example session, snapshot 1.}
-  {Example session, snapshot 1.}
+\myincludegraphics{step1}{t}{12cm}{Example session.}
+  {Example session.}
 %\myincludegraphics{step2}{t}{4cm}{Example session, snapshot 2.}
 % {Example session, snapshot 2.}
 
@@ -270,7 +270,7 @@ of the window in background in Fig. \ref{step1}.
 While the user is wondering how to proceed in the proof, the tutors are
 trying to progress in the proof. After a while, the tutors' suggestions
 start to appear in the lower part of the \hbugs{} interface window
-(the topmost window in Fig. \ref{prima}). In this case, the tutors are able
+(the topmost window in Fig. \ref{step1}). In this case, the tutors are able
 to produce 23 hints. The first and not very useful hint suggests to proceed in
 the proof by exchanging the two sides of the equality.
 The second hint suggests to reduce both sides of the equality to their normal