From 383c0e6ff61664272e765bb05eb10565b66c5587 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 17 Nov 2005 10:13:22 +0000 Subject: [PATCH] fixed some stuff in the patterns section --- helm/papers/matita/Makefile | 4 ++-- helm/papers/matita/matita.tex | 25 +++++++++++++++---------- 2 files changed, 17 insertions(+), 12 deletions(-) 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} -- 2.39.2