Commit 0c1dfd77 authored by Asma Tafat-Bouzid's avatar Asma Tafat-Bouzid

Latex documentation

parent 9d83a21e
......@@ -496,6 +496,12 @@ not and you have to use the IDE to update it.
HTML syntax.
\end{itemize}
About \texttt{latex} output, we propose another option
\texttt{-latex2} with the same parameters. The difference between
these two options is the layout of the tabular.
Generated \latex files contain a set of macros. Definitions of these macros is left to the care of user depending on what he wants, or not, highlight.
\section{The \texttt{why3.conf} configuration file}
\label{sec:whyconffile}
One can use a custom configuration file. \texttt{why3config}
......
......@@ -133,6 +133,4 @@ assert (h: x=0 \/ 0 < x) by omega.
apply Parent_inf_el with (n := n);
auto with zarith.
Qed.
(* DO NOT EDIT BELOW *)
(* DO NOT EDIT BELOW *)
\ No newline at end of file
......@@ -317,6 +317,4 @@ assert (h: (i = j-1 \/ i < j-1)%Z) by omega.
rewrite H_induc; auto with zarith.
unfold sorted_sub; auto with zarith.
Qed.
(* DO NOT EDIT BELOW *)
(* DO NOT EDIT BELOW *)
\ No newline at end of file
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