From d04c51d4a69b0dc4838f46a41b4018835b252ff8 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 31 Jan 2006 16:07:04 +0000
Subject: [PATCH] use math mode when referencing terms from a \sequent
 environment

---
 helm/papers/matita/matita2.tex | 35 ++++++++++++----------------------
 1 file changed, 12 insertions(+), 23 deletions(-)

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 88f664c2d..494b1c25a 100644
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -1284,9 +1284,9 @@ Take for instance the statement:
 Possible legal names are: \texttt{plus\_n\_O}, \texttt{plus\_O}, 
 \texttt{eq\_n\_plus\_n\_O} and so on.
 
-Similarly, consider the theorem:
+Similarly, consider the statement
 \begin{grafite}
- \forall n, m: nat. n < m to n \leq m
+\forall n, m: nat. n < m to n \leq m
 \end{grafite}
 In this case \texttt{lt\_to\_le} is a legal name, 
 while \texttt{lt\_le} is not.
@@ -1325,7 +1325,7 @@ The other special case is that of statements whose conclusion is a
 match expression. 
 A typical example is the following:
 \begin{grafite}
-\forall n,m:nat. 
+\forall n, m: nat. 
   match (eqb n m) with
   [ true  \Rightarrow n = m 
   | false \Rightarrow n \neq m]
@@ -1506,40 +1506,29 @@ second searches the \NT{wanted} term starting from that roots.
 \end{description}
 
 \subsubsection{Examples}
-%To explain how the first phase works let us give an example. Consider
-%you want to prove the uniqueness of the identity element $0$ for natural
-%sum, and that you can rely on the previously demonstrated left
-%injectivity of the sum, that is $inj\_plus\_l:\forall x,y,z.x+y=z+y \to x =z$.
-%Typing
-%\begin{grafite}
-%theorem valid_name: \forall n,m. m + n = n \to m = O.
-%  intros (n m H).
-%\end{grafite}
 
 Consider the following sequent:
 \sequent{n: nat\\m: nat\\H: m + n = n}{m = O}
 
-To change the right part of the equality of the \texttt{H}
-hypothesis with \texttt{O + n}, the user selects and pastes it as the pattern
+To change the right part of the equality of the $H$
+hypothesis with $O + n$, the user selects and pastes it as the pattern
 in the following statement.
 \begin{grafite}
   change in H:(? ? ? %) with (O + n).
 \end{grafite}
 
-To understand the pattern (or produce it by hand) the user should be
-aware that the notation \texttt{m + n = n} hides the term
-\texttt{eq nat (m + n) n}, so
-that the pattern selects only the third argument of \texttt{eq}.
+To understand the pattern (or produce it by hand) the user should be aware that
+the notation $m + n = n$ hides the term $\mathrm{eq}~\mathrm{nat}~(m + n)~n$, so
+that the pattern selects only the third argument of $\mathrm{eq}$.
 
-The experienced user may also write by hand a concise pattern
-to change at once all the occurrences of \texttt{n} in the hypothesis
-\texttt{H}:
+The experienced user may also write by hand a concise pattern to change at once
+all the occurrences of $n$ in the hypothesis $H$:
 \begin{grafite}
   change in H match n with (O + n).
 \end{grafite}
 
-In this case the \NT{sequent\_path} selects the whole \texttt{H}, while
-the second phase locates \texttt{n}.
+In this case the \NT{sequent\_path} selects the whole $H$, while
+the second phase locates $n$.
 
 The latter pattern is equivalent to the following one, that the system
 can automatically generate from the selection.
-- 
2.39.5