From: Claudio Sacerdoti Coen Date: Fri, 30 May 2003 15:09:45 +0000 (+0000) Subject: ... X-Git-Tag: submitted~6 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b0d9f83fe0b38e6aa562998cf0c6053444541a91;p=helm.git ... --- 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