final ispell

diff --git a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex
index 2625d6b7d2098a927aaf71d410e8306036baf4ad..dd2ad61e8c13b7b29f752bffe71a5f13b939dda1 100644 (file)
--- a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex
+++ b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex
@@ -295,18 +295,18 @@ the user the scalar to use as an argument of the previous lemma; the second
 one states that the scalar is different from 0; the third lemma (the main
 one) asks to prove the equality between the two new members.
 % is shown in Fig. \ref{step2} where $?_3[H;x]$ stands for
-% the still unkown scalar argument, which can have only $H$ and $x$ as
+% the still unknown scalar argument, which can have only $H$ and $x$ as
 % free variables.
 
-The user proceeds by istantiating the scalar with the number 2. The
+The user proceeds by instantiating the scalar with the number 2. The
 \texttt{Assumption} tutor now suggests to close the second goal (that
 states that $2 \neq 0$) by applying the hypothesis $H$.
 No useful suggestions, instead, are generated for the main goal
 $2*x = 2*((x+1)*(x+1)-1-x*x)*2^{-1}$.
-To proceed in the proof the user needs to symplify the
+To proceed in the proof the user needs to simplify the
 expression using the lemma $Rinv\_r\_simpl\_m$ that states that
 $\forall x,y.\;y = x * y * x^{-1}$. Since we do not provide yet any tutor
-suggesting symplifications, the user must find out this symplication by
+suggesting simplifications, the user must find out this simplification by
 himself. Once she founds it, the goal is reduced to proving that
 $2*x = (x+1)*(x+1) - 1 - x*x$. This equality is easily solved by the
 \texttt{Ring} tutor, that suggests\footnote{The \texttt{Ring} suggestion is