Commit 6bc8c646 authored by MARCHE Claude's avatar MARCHE Claude

doc

parent e9a5d7d4
\chapter{The Why3 Application Programming Interface}
\section{Building Terms and Formulas}
\section{Building Theories}
\section{Buildings Tasks and calling External Provers}
\section{Applying transformations}
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End:
...@@ -3,3 +3,10 @@ ...@@ -3,3 +3,10 @@
\section{IDE} \section{IDE}
hello hello
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End:
\chapter{Reference manuals for the Why3 tools}
\section{Compilation, Installation}
\section{The \texttt{why.conf} configuration file}
\section{The \texttt{why3} command-line tool}
\section{The \texttt{why3ml} tool}
\section{The \texttt{why3ide} tool}
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End:
...@@ -2,8 +2,26 @@ ...@@ -2,8 +2,26 @@
\begin{document} \begin{document}
\chapter{Syntax} \title{Why3 manual}
\author{F. Bobot \and J.-C. Filli\^atre \and C. March\'e \and A. Paskevich}
\maketitle
\cleardoublepage
\tableofcontents
\input{syntax.tex}
\input{ide.tex} \input{ide.tex}
\input{api.tex}
\input{manpages.tex}
\end{document} \end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: t
%%% End:
\chapter{Syntax}
This chapter describes the input syntax, and informally gives its semantics,
illustrated by examples.
\section{Terms and Formulas}
\section{Declarations, Theories}
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End:
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