From b0d9f83fe0b38e6aa562998cf0c6053444541a91 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 30 May 2003 15:09:45 +0000 Subject: [PATCH] ... --- helm/papers/calculemus-2003/hbugs-calculemus-2003.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex index 22036320c..ae81aba67 100644 --- a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex +++ b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex @@ -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 -- 2.39.2