fixed some stuff in the patterns section

[helm.git] / helm / papers / matita / matita.tex

diff --git a/helm/papers/matita/matita.tex b/helm/papers/matita/matita.tex
index 205333113b9538144de215e338573795b7aec49a..ff307e80fcac3b657baa5670bcfb1f185d004157 100644 (file)
--- a/helm/papers/matita/matita.tex
+++ b/helm/papers/matita/matita.tex
@@ -275,7 +275,7 @@ selects roots (subterms) of the sequent, using the
 $\NT{sequent\_path}$,  while the second 
 one searches the $\NT{wanted}$ term starting from these roots. Both are
 optional steps, and by convention the empty pattern selects the whole
-goal.
+conclusion.
 
 \begin{description}
 \item[Phase 1]
@@ -379,9 +379,10 @@ following one, that is less readable but uses only the first phase.
 \noindent
 
 \subsubsection{Tactics supporting patterns}
-In \MATITA{} the following tactics can be restricted to subterms of
-the working sequent: simplify, change, fold, unfold, generalize, replace and
-rewrite.
+In \MATITA{} all the tactics that can be restricted to subterm of the working
+sequent accept the pattern syntax. In particular these tactics are: simplify,
+change, fold, unfold, generalize, replace and rewrite.
+
 \NOTE{attualmente rewrite e \\ fold non supportano \\ phase 2. per
 supportarlo\\bisogna far loro trasformare\\il pattern phase1+phase2\\
 in un pattern phase1only\\come faccio nell'ultimo esempio.\\lo si fa
@@ -437,12 +438,12 @@ 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, 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
-mouse to select the wanted term is probably the only way to tell the
-system exactly what you want to do. 
+from the idea behind patterns, but really fails in extending to
+complex notation, since it relays on a mono-dimensional sequent representation.
+Real math notation places arguments upside-down (like in indexed sums or
+integrations) or even puts them inside a bidimensional matrix.  
+In these cases using the mouse to select the wanted term is probably the 
+only way to tell the system exactly what you want to do. 
 
 One of the goals of \MATITA{} is to use modern publishing techiques, and
 adopting a method for restricting tactics application domain that discourages 
@@ -451,6 +452,10 @@ using heavy math notation, would definitively be a bad choice.
 \subsection{tatticali}
 \ASSIGNEDTO{gares}
 
+\begin{verbatim}
+
+\end{verbatim}
+
 \subsection{Disambiguation}
 \label{sec:disambiguation}
 \ASSIGNEDTO{zack}