fixed some stuff in pattern section

diff --git a/helm/papers/matita/matita.tex b/helm/papers/matita/matita.tex
index 506d43167596abe2df3fce44b305ccca2ee7412c..205333113b9538144de215e338573795b7aec49a 100644 (file)
--- a/helm/papers/matita/matita.tex
+++ b/helm/papers/matita/matita.tex
@@ -60,7 +60,7 @@
   \savebox{\tmpxyz}[0.9\linewidth]{
     \begin{minipage}{0.9\linewidth}
       \ensuremath{#1} \\
-      --------------------------\\ % come si fa una linea orizzontale?
+      \rule{3cm}{0.03cm}\\
       \ensuremath{#2}
     \end{minipage}}\setlength{\fboxsep}{3mm}%
   \begin{center}
@@ -238,7 +238,7 @@ selection.
 Matita benefits of a graphical interface and a powerful MathML rendering
 widget that allows the user to select pieces of the sequent he is working
 on. While this is an extremely intuitive way for the user to
-restrict the application of a tactic, for example, to some subterms of the
+restrict the application of tactics, for example, to some subterms of the
 conclusion or some hypothesis, the way this action is recorded to the text
 script is not obvious.\\
 In \MATITA{} this issue is addressed by patterns.
@@ -246,7 +246,7 @@ In \MATITA{} this issue is addressed by patterns.
 \subsubsection{Pattern syntax}
 A pattern is composed of two terms: a $\NT{sequent\_path}$ and a
 $\NT{wanted}$.
-The former mocks-up a sequent, replacing unwanted subterms with $?$ and
+The former mocks-up a sequent, discharging unwanted subterms with $?$ and
 selecting the interesting parts with the placeholder $\%$. 
 The latter is a term that lives in the context of the placeholders.
 
@@ -349,15 +349,14 @@ hypothesis with $O + n$ and then use $inj\_plus\_l$ to prove $m=O$.
 \end{grafite}
 \noindent
 This pattern, that is a simple instance of the $\NT{sequent\_path}$
-grammar entry, acts on $H$ that has type (without notation) 
-$(eq~nat~(m+n)~n)$ and discharges the head of the application and the
-first two arguments with a $?$ and selects the last argument with
-$\%$. The syntax may seem uncomfortable, but the user can simply
-select with the mouse the right part of the equivalence and left to the
-system the burden of writing down in the script file the corresponding 
-pattern with $?$ and $\%$ in the right place (expecially where implicit
-arguments are hidden by the notation, like the type $nat$ in this
-example).
+grammar entry, acts on $H$ that has type (without notation) $(eq~nat~(m+n)~n)$
+and discharges the head of the application and the first two arguments with a
+$?$ and selects the last argument with $\%$. The syntax may seem uncomfortable,
+but the user can simply select with the mouse the right part of the equivalence
+and left to the system the burden of writing down in the script file the
+corresponding pattern with $?$ and $\%$ in the right place (that is not
+trivial, expecially where implicit arguments are hidden by the notation, like
+the type $nat$ in this example).
 
 Changing all the occurrences of $n$ in the hypothesis $H$ with $O+n$ 
 works too and can be done, by the experienced user, writing directly
@@ -406,7 +405,7 @@ occurce of it (counting from left to right). In our previous example,
 to change only the left part of the equivalence, the correct command
 is
 \begin{grafite}
-  change n at 2 in H with (O + H)
+  change n at 2 in H with (O + n)
 \end{grafite} 
 \noindent
 meaning that in the hypothesis $H$ the $n$ we want to change is the
@@ -438,7 +437,7 @@ but for example not for change and other tactics that do not relay on
 unification. 
 
 The idea behind this way of identifying subterms in not really far
-from the idea behind patterns patterns, but really fails in help using
+from the idea behind patterns, but really fails in help using
 complex notation, since it relays on the way the user sees the
 sequent.  Notation can swap arguments, or place them upside-down or
 even put them inside a bidimensional matrix.  In these cases using the