Big commit to let Ferruccio try the merge_coercion patch.

[helm.git] / helm / ocaml / tactics / doc / body.tex

diff --git a/helm/ocaml/tactics/doc/body.tex b/helm/ocaml/tactics/doc/body.tex
index 424dee225871b7188ae0e7b3ad53080d316fb4ba..8b7bbc9b043d1aa3a679131050c593ca1d17afd2 100644 (file)
--- a/helm/ocaml/tactics/doc/body.tex
+++ b/helm/ocaml/tactics/doc/body.tex
@@ -17,13 +17,13 @@ like Coq, Isabelle, PhoX, LEGO, and many more. Other system specific GUIs exist
 but share the same design, understanding it and they way such GUIs are operated
 is relevant to our discussion.
 
-\begin{figure}[ht]
- \begin{center}
-  \resizebox{\textwidth}{!}{\includegraphics{pics/pg-coq-screenshot}}
-  \caption{Proof General: a generic interface for proof assistants}
-  \label{fig:proofgeneral}
- \end{center}
-\end{figure}
+%\begin{figure}[ht]
+% \begin{center}
+%  \includegraphic{pics/pg-coq-screenshot}
+%  \caption{Proof General: a generic interface for proof assistants}
+%  \label{fig:proofgeneral}
+% \end{center}
+%\end{figure}
 
 % - modo di lavorare
 
@@ -52,42 +52,42 @@ minus with natural plus, along with its proof (line numbers have been added for
 the sake of presentation) as it can be found in the standard library of the
 \MATITA{} proof assistant:
 
-\begin{example}
-\begin{Verbatim}
-theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
- intros.
- cut (m+p \le n \or m+p \nleq n).
- elim Hcut.
- symmetry.
- apply plus_to_minus.
- rewrite > assoc_plus.
- rewrite > (sym_plus p).
- rewrite < plus_minus_m_m.
- rewrite > sym_plus.
- rewrite < plus_minus_m_m.
- reflexivity.
- apply (trans_le ? (m+p)).
- rewrite < sym_plus.
- apply le_plus_n.
- assumption.
- apply le_plus_to_minus_r.
- rewrite > sym_plus.
- assumption.   
- rewrite > (eq_minus_n_m_O n (m+p)).
- rewrite > (eq_minus_n_m_O (n-m) p).
- reflexivity.
- apply le_plus_to_minus.
- apply lt_to_le.
- rewrite < sym_plus.
- apply not_le_to_lt.
- assumption.
- apply lt_to_le.
- apply not_le_to_lt.
- assumption.          
- apply (decidable_le (m+p) n).
-qed.
-\end{Verbatim}
-\end{example}
+%\begin{example}
+%\begin{Verbatim}
+%theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
+% intros.
+% cut (m+p \le n \or m+p \nleq n).
+% elim Hcut.
+% symmetry.
+% apply plus_to_minus.
+% rewrite > assoc_plus.
+% rewrite > (sym_plus p).
+% rewrite < plus_minus_m_m.
+% rewrite > sym_plus.
+% rewrite < plus_minus_m_m.
+% reflexivity.
+% apply (trans_le ? (m+p)).
+% rewrite < sym_plus.
+% apply le_plus_n.
+% assumption.
+% apply le_plus_to_minus_r.
+% rewrite > sym_plus.
+% assumption.   
+% rewrite > (eq_minus_n_m_O n (m+p)).
+% rewrite > (eq_minus_n_m_O (n-m) p).
+% reflexivity.
+% apply le_plus_to_minus.
+% apply lt_to_le.
+% rewrite < sym_plus.
+% apply not_le_to_lt.
+% assumption.
+% apply lt_to_le.
+% apply not_le_to_lt.
+% assumption.          
+% apply (decidable_le (m+p) n).
+%qed.
+%\end{Verbatim}
+%\end{example}
 
 The script snippet is made of 32 statements, one per line (but this is not a
 requirement of the \MATITA{} script language, namely \emph{Grafite}). The first
@@ -103,13 +103,13 @@ replaying) the above script, the user may position it at the end of any line,
 having feedback about the status of the proof in that point. See for example
 Fig.~\ref{fig:matita} where an intermediate proof status is shown.
 
-\begin{figure}[ht]
- \begin{center}
-  \resizebox{\textwidth}{!}{\includegraphics{matita_screenshot}}
-  \caption{Matita: ongoing proof}
-  \label{fig:matita}
- \end{center}
-\end{figure}
+%\begin{figure}[ht]
+% \begin{center}
+%  \includegraphic{matita_screenshot}
+%  \caption{Matita: ongoing proof}
+%  \label{fig:matita}
+% \end{center}
+%\end{figure}
 
 % - script: sorgenti di un linguaggio imperativo, oggetti la loro semantica
 % - script = sequenza di comandi
@@ -193,11 +193,11 @@ Finally, the branching constructs \texttt{[}, \texttt{|}, and \texttt{]} enable
 proof structuring. Consider for example an alternative, branching based, version
 of the example above:
 
-\begin{example}
-\begin{Verbatim}
-...
-\end{Verbatim}
-\end{example}
+%\begin{example}
+%\begin{Verbatim}
+%...
+%\end{Verbatim}
+%\end{example}
 
 Tactic applications are the same of the previous version of the script, but
 branching tacticals are used. The above version is highly more readable and