Typos

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 9dca4c67768a9c5db5fdef044a3186be63d3a28e..464e66c0d8ea43de02e75e3e2b739b4aa8af042e 100644 (file)
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -764,9 +764,9 @@ library. To this aim, Matita uses a sophisticated indexing mechanism
 for mathemtical items, based on a reach metadata set that has been 
 tuned along the European Project IST-2001-33562 MoWGLI. The metadata
 set, and the searching facilites built on top of them - collected 
-in the so called \whelp seach engine - have been
+in the so called \WHELP search engine - have been
 extensively described in \cite{whelp}. Let us just recall here that
-the whelp metadata model is essentially based a single ternary relation 
+the \WHELP metadata model is essentially based a single ternary relation 
 \REF{p}{s}{t} stating that an object $s$ refers an object $t$ at a
  given position $p$, where the position specify the place of the 
 occurrence of $t$ inside $s$ (we currently work with a fixed set of 
@@ -787,18 +787,18 @@ A first, very simple but not negligeable feature is the check for duplicates.
 As soon as a new statement is defined, and before proving it, 
 the library is searched 
 to check that no other equivalent statement has been already proved
-(based on the \whelp{} pattern matching functionality); if this is the case,
+(based on the \WHELP pattern matching functionality); if this is the case,
 a warning is raised to the user. At present, the notion of equivalence 
 adopted by Matita is convertibility, but we may imagine to weaken it 
 in the future, covering for instance isomorphisms.    
 
-Another usefull \whelp{} operation is {\em hint}; we may invoke this query
+Another usefull \WHELP operation is {\em hint}; we may invoke this query
 at any moment during the development of a proof, resulting in the list
 of all theorems of the library which can be applied to the current
 goal. In practice, this is mostly used not really to discover what theorems
 can be applied to a given goal, but to actually retrieve a theorem that 
 we wish to apply, but whose name we have forgotten.
-In fact, even if \Matita adopts a semi-rigid naming convention for 
+In fact, even if \MATITA adopts a semi-rigid naming convention for 
 statements \ref{naming} that greatly simplifies the effort of recalling
 names, the naming discipline remains one of the most
 annoying aspects of formal developments, and the hint feature provides