use math mode when referencing terms from a \sequent environment

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

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 88f664c2dcbf911e5acffd7fa2d8841a184f4077..494b1c25a7bf2bd5ba54a37b4cc595b9cb023f32 100644 (file)
--- 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.
 
 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}
 \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.
 \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}
 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]
   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}
 \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}
 
 
 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}
 
 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}
 
 \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.
 
 The latter pattern is equivalent to the following one, that the system
 can automatically generate from the selection.