]> matita.cs.unibo.it Git - helm.git/commitdiff
...
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 30 May 2003 15:09:45 +0000 (15:09 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 30 May 2003 15:09:45 +0000 (15:09 +0000)
helm/papers/calculemus-2003/hbugs-calculemus-2003.tex

index 22036320c318cc0a0117ca56dc0db0936f8c8ca2..ae81aba67494e65acd68b0d9a811deec74176f6c 100644 (file)
@@ -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