From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 17 Nov 2005 10:13:22 +0000 (+0000)
Subject: fixed some stuff in the patterns section
X-Git-Tag: V_0_7_2_3~56
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=383c0e6ff61664272e765bb05eb10565b66c5587

fixed some stuff in the patterns section
---

diff --git a/helm/papers/matita/Makefile b/helm/papers/matita/Makefile
index bfae83c3a..d287d115c 100644
--- 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 
-BUILD_FORMATS = dvi
+BUILD_FORMATS = dvi ps
 
 # which format to be shown on "make show"
 SHOW_FORMAT = dvi
@@ -112,7 +112,7 @@ else
 	$(DVIPDF) $< $@
 endif
 %.ps: %.dvi
-	$(DVIPS) $<
+	$(DVIPS) -ta4 $<
 %.ps.gz: %.ps
 	$(GZIP) -c $< > $@
 %.html: %.tex
diff --git a/helm/papers/matita/matita.tex b/helm/papers/matita/matita.tex
index 205333113..ff307e80f 100644
--- 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}