fixed some stuff in the patterns section

diff --git a/helm/papers/matita/Makefile b/helm/papers/matita/Makefile
index bfae83c3ab7e96356b3c2ad5759782f68485717d..d287d115c6811646d5f066afdd2f7eda46a754d5 100644 (file)
--- a/helm/papers/matita/Makefile
+++ b/helm/papers/matita/Makefile
@@ -25,7 +25,7 @@ PDF_VIA_PDFLATEX = yes
 # which formats generated by default ("all" target)?
 # (others will be generated by "world" target)
 # see AVAILABLE_FORMATS below 
 # which formats generated by default ("all" target)?
 # (others will be generated by "world" target)
 # see AVAILABLE_FORMATS below 

-BUILD_FORMATS = dvi
+BUILD_FORMATS = dvi ps

 
 # which format to be shown on "make show"
 SHOW_FORMAT = dvi
 
 # which format to be shown on "make show"
 SHOW_FORMAT = dvi


@@ -112,7 +112,7 @@ else
        $(DVIPDF) $< $@
 endif
 %.ps: %.dvi
        $(DVIPDF) $< $@
 endif
 %.ps: %.dvi

-       $(DVIPS) $<
+       $(DVIPS) -ta4 $<

 %.ps.gz: %.ps
        $(GZIP) -c $< > $@
 %.html: %.tex
 %.ps.gz: %.ps
        $(GZIP) -c $< > $@
 %.html: %.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
 $\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]
 
 \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}
 \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
 \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
 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 
 
 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}
 
 \subsection{tatticali}
 \ASSIGNEDTO{gares}
 

+\begin{verbatim}
+
+\end{verbatim}
+

 \subsection{Disambiguation}
 \label{sec:disambiguation}
 \ASSIGNEDTO{zack}
 \subsection{Disambiguation}
 \label{sec:disambiguation}
 \ASSIGNEDTO{zack}