Commit 659597a2 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Ensure that tool pictures are centered in the HTML documentation.

parent 90a9ab7a
......@@ -34,6 +34,7 @@ friendly way. This section presents the basic use of this GUI. Please
refer to Section~\ref{sec:ideref} for a more complete description.
\begin{figure}[tbp]
%HEVEA\centering
\includegraphics[width=\textwidth]{gui-0-70-1.png}
\caption{The GUI when started the very first time}
\label{fig:gui1}
......@@ -65,6 +66,7 @@ contains one theory, itself containg three goals.
\begin{figure}[tbp]
%HEVEA\centering
\includegraphics[width=\textwidth]{gui-0-70-2.png}
\caption{The GUI with goal G1 selected}
\label{fig:gui2}
......@@ -87,6 +89,7 @@ click on the \textsf{Simplify} button. After a short time, you should
get the display of Figure~\ref{fig:gui3}.
\begin{figure}[tbp]
%HEVEA\centering
\includegraphics[width=\textwidth]{gui-0-70-3.png}
\caption{The GUI after Simplify prover is run on each goal}
\label{fig:gui3}
......@@ -112,6 +115,7 @@ Simplify. We already have a lot of goals and proof attempts, so it is a good ide
You should see now what is displayed on Figure~\ref{fig:gui4}.
\begin{figure}[tbp]
%HEVEA\centering
\includegraphics[width=\textwidth]{gui-0-70-4.png}
\caption{The GUI after splitting goal $G_2$ and collapsing proved goals}
\label{fig:gui4}
......@@ -133,6 +137,7 @@ part you modify, in order to regenerate the file if the goal is
changed.
\begin{figure}[tbp]
%HEVEA\centering
\includegraphics[width=\textwidth]{coqide-0-70.png}
\caption{CoqIDE on subgoal 1 of $G_2$}
\label{fig:coqide}
......@@ -154,6 +159,7 @@ false, \eg
We can reload the modified file in the IDE using menu \textsf{File/Reload}, or the shortcut ``Ctrl-R''. We get the tree view shown on Figure~\ref{fig:gui5}.
\begin{figure}[tbp]
%HEVEA\centering
\includegraphics[width=\textwidth]{gui-0-70-5.png}
\caption{File reloaded after modifying goal $G_2$}
\label{fig:gui5}
......@@ -183,7 +189,7 @@ Notice that replaying can be done in batch mode, using the
\texttt{why3replayer} tool (see Section~\ref{sec:why3replayer}) For
example, running the replayer on the \texttt{hello\_proof} example is
as follows (assuming $G_2$ still is
\lstinline{(true -> false) /\ (true \/ false)}).
\lstinline|(true -> false) /\ (true \/ false)|).
\begin{verbatim}
$ why3replayer hello_proof
Info: found directory 'hello_proof' for the project
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment