X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fdoc%2Fbody.tex;h=8b7bbc9b043d1aa3a679131050c593ca1d17afd2;hb=93703370bfac25b4d342278388f54cc5e27cd531;hp=424dee225871b7188ae0e7b3ad53080d316fb4ba;hpb=5fd3862ee12950c8441a313bdc1e0c2cb4078cf0;p=helm.git

diff --git a/helm/ocaml/tactics/doc/body.tex b/helm/ocaml/tactics/doc/body.tex
index 424dee225..8b7bbc9b0 100644
--- 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