spell checking

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 494b1c25a7bf2bd5ba54a37b4cc595b9cb023f32..4883fa4ad1b04802b7f8c8ba16dc161d026067e0 100644 (file)
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -817,7 +817,7 @@ effective way, assuming as little knowledge as possible about the
 library. To this aim, \MATITA{} uses a sophisticated indexing mechanism
 for mathematical concepts, based on a rich metadata set that has been 
 tuned along the European project \MOWGLIIST{} \MOWGLI. The metadata
-set, and the searching facilites built on top of them --- collected 
+set, and the searching facilities built on top of them --- collected 
 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 
@@ -837,7 +837,7 @@ sections rely in a direct or indirect way on its metadata system and
 the search features. Here, we shall just recall some of its most
 direct applications.
 
-A first, very simple but not negligeable feature is the \emph{duplicate check}.
+A first, very simple but not negligible feature is the \emph{duplicate check}.
 As soon as a theorem is stated, just before starting its proof, 
 the library is searched 
 to check that no other equivalent statement has been already proved
@@ -910,10 +910,10 @@ specified terms. In case of overloaded sources there exists multiple aliases
 with the same source. It is possible to record \emph{disambiguation
 preferences} to select one of the aliases of an overloaded source.
 
-Preferences can be explicitely given in the script (using the
+Preferences can be explicitly given in the script (using the
 misleading \texttt{alias} commands), but
 are also implicitly added when a new concept is introduced (\emph{implicit
-preferences}) or after a sucessfull disambiguation that did not require
+preferences}) or after a successful disambiguation that did not require
 user interaction. Explicit preferences are added automatically by \MATITA{} to
 record the disambiguation choices of the user. For instance, after the
 disambiguation of the command above, the script is altered as follows:
@@ -940,7 +940,7 @@ status.  Unlike aliases, they are not part of the library.
 When starting a new authoring session the set of disambiguation preferences
 is empty. Until it contains a preference for each overloaded symbol to be
 used in the script, the user can be faced with questions from the disambiguator.
-To reduce the likelyhood of user interactions, we introduced
+To reduce the likelihood of user interactions, we introduced
 the \texttt{include} command. With \texttt{include} it is possible to import
 at once in the current session the set of preferences that was in effect
 at the end of the execution of a given script.
@@ -1037,7 +1037,7 @@ partially specified term where in place of \texttt{n} the application of a
 coercion from \texttt{nat} to \texttt{R} appears (assuming such a coercion has
 been defined in advance).
 
-Implicitc coercions are not always desirable. For example, in disambiguating
+Implicit coercions are not always desirable. For example, in disambiguating
 \texttt{\TEXMACRO{forall} x: nat. n < n + 1} we do not want the term which uses
 2 coercions from \texttt{nat} to \texttt{R} around \OP{<} arguments to show up
 among the possible partially specified term choices. For this reason we always
@@ -1219,7 +1219,7 @@ The former derives new facts by a set of active
 facts and a new \emph{given} clause suitably selected from a set of passive
 equations. The latter tries to simplify the equations
 orienting them according to a suitable weight associated to terms.
-\MATITA{} currently supports several different weigthing functions
+\MATITA{} currently supports several different weighting functions
 comprising Knuth-Bendix ordering (kbo) and recursive path ordering (rpo), 
 that integrates particularly well with normalization.
 
@@ -1589,7 +1589,7 @@ x.(H~x)\to (P~x)$) will unify \texttt{x} with \texttt{n} and \texttt{P} with
 
 Since \TAC{rewrite}, \TAC{replace} and several other tactics boils down to
 the application of the equality elimination principle, the previous
-trick implements the expected behaviour.
+trick implements the expected behavior.
 
 The idea behind this way of identifying subterms in not really far
 from the idea behind patterns, but fails in extending to
@@ -1605,7 +1605,7 @@ using heavy math notation would have definitively been a bad choice.
 
 In \MATITA{}, tactics accepting pattern arguments can be more expressive than
 the equivalent tactics in \COQ{} since variables bound in the pattern context,
-can occurr in context-dependent arguments. For example, consider the sequent:
+can occur in context-dependent arguments. For example, consider the sequent:
 \sequent{n: nat\\x: nat\\H: \forall m. n + m*n = x + m}{m = O}
 In \MATITA{} the user can issue the command:
 \begin{grafite}
@@ -1765,7 +1765,7 @@ scripts, listed in Tab.~\ref{tab:scripts}.
 
 We do not plan to maintain the library in a centralized way, 
 as most of the systems do. On the contrary we are currently
-developing wiki-technologies to support collaborative 
+developing Wiki-technologies to support collaborative 
 development of the library, encouraging people to expand, 
 modify and elaborate previous contributions.