diff --git a/Makefile.in b/Makefile.in
index 7cd9a44427734308e33ab8b4f6cddac5afed8649..6648272ec0108ab2c1c506bf9dba502d51090b5e 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -1464,9 +1464,9 @@ doc/bnf: doc/bnf.mll
 	$(OCAMLLEX) $<
 	$(OCAMLOPT) -o $@ doc/bnf.ml
 
-DOC = api glossary ide intro library macros manpages install coq_tactic \
-      realizations manual starting syntax syntaxref technical version whyml \
-      pvs
+DOC = api glossary ide intro library macros manpages install \
+      manual starting syntax syntaxref technical version whyml \
+      itp pvs coq coq_tactic isabelle
 
 DOCTEX = $(addprefix doc/, $(addsuffix .tex, $(DOC)))
 
diff --git a/doc/coq.tex b/doc/coq.tex
index 40a49cedb44f022805a05452a177ef980b4151a6..011dad179d82d220c63764a77801552bc836c3f5 100644
--- a/doc/coq.tex
+++ b/doc/coq.tex
@@ -1,6 +1,7 @@
 
-\subsection{Coq}
+\section{Coq}
 \label{sec:coq}
+\index{Coq proof assistant}
 
 This section describes the content of the Coq files generated by \why for
 both proof obligations and theory realizations. When reading a Coq
@@ -40,3 +41,10 @@ Currently, the parser for Coq scripts is rather naive and does not know
 much about comments. For instance, \why can easily be confused by
 some terminating directive like \verb+Qed+ that would be present in a
 comment.
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-PDF-mode: t
+%%% TeX-master: "manual"
+%%% End:
diff --git a/doc/coq_tactic.tex b/doc/coq_tactic.tex
index 45a541f0084a730269c7f6a7b3cf1e889a423a06..5340a12331fd7681a42aebb082d0171dcaa00847 100644
--- a/doc/coq_tactic.tex
+++ b/doc/coq_tactic.tex
@@ -1,10 +1,9 @@
-\chapter{Coq Tactic}
-\label{chap:tactic}
-\index{Coq proof assistant}
+\subsection{Coq Tactic}
+\label{sec:coqtactic}
 
 \why\ provides a Coq tactic to call external theorem provers as oracles.
 
-\section{Installation}
+\subsubsection{Installation}
 
 You need Coq version 8.3 or greater. If this is the case, \why's
 configuration detects it, then compiles and installs the Coq tactic.
@@ -24,7 +23,7 @@ option \texttt{-I} or by adding
 \end{center}
 to your \texttt{\~{}/.coqrc} resource file.
 
-\section{Usage}
+\subsubsection{Usage}
 
 The Coq tactic is called \texttt{why3} and is used as follows:
 \begin{center}
@@ -41,7 +40,7 @@ limit in seconds as given by \why's configuration file
 (see page~\pageref{sec:whyconffile}). A different value may be given
 using the \texttt{timelimit} keyword.
 
-\paragraph{Error messages.} The following errors may be reported by
+\subsubsection{Error messages.} The following errors may be reported by
 the Coq tactic.
 \begin{description}
 \item[\texttt{Not a first order goal}]\emptyitem
diff --git a/doc/install.tex b/doc/install.tex
index 74cd20d558ab84656d93b6a9f49a5680ee1b5d6c..ade1a2348d382c70f99868f8a0aab830212519df 100644
--- a/doc/install.tex
+++ b/doc/install.tex
@@ -53,13 +53,14 @@ It is also installable from sources, available from the site
 \end{itemize}
 
 
-If you want to use the specific Coq features, \ie the Coq
-tactic~\ref{chap:tactic} and Coq realizations~\ref{sec:realizations},
-then Coq has to be installed before \why. Look at the summary printed
-at the end of the configuration script to check if Coq has been
-detected properly. Similarly, for using PVS or Isabelle to discharge proofs, PVS
-and Isabelle must be installed before \why. You should check that
-those proof assistants are correctly detected by the configure script.
+If you want to use the specific Coq features, \ie the Coq tactic
+(Section~\ref{sec:coqtactic}) and Coq realizations
+(Section~\ref{sec:realizations}), then Coq has to be installed before
+\why. Look at the summary printed at the end of the configuration
+script to check if Coq has been detected properly. Similarly, for
+using PVS (Section~\ref{sec:pvs}) or Isabelle (Section~\ref{sec:isabelle}) to discharge proofs, PVS and Isabelle must be
+installed before \why. You should check that those proof assistants
+are correctly detected by the configure script.
 
 When configuration is finished, you can compile \why.
 \begin{verbatim}
@@ -71,7 +72,7 @@ make install
 \end{verbatim}
 Installation can be tested as follows: 
 \begin{enumerate}
-\item install some external provers (see~Section\ref{provers} below)
+\item install some external provers (see~Section~\ref{provers} below)
 \item run \verb|why3config --detect|
 \item run some examples from the distribution, \eg you should
 obtain the following:
diff --git a/doc/isabelle.tex b/doc/isabelle.tex
index 8b0676a0a395e3820e8a78dde8cf4023d97c8611..2803b6c4b0ec8be2f00f6bbc8ec8dbf9e6b6cb77 100644
--- a/doc/isabelle.tex
+++ b/doc/isabelle.tex
@@ -1,12 +1,23 @@
-\subsection{Isabelle/HOL}
+\section{Isabelle/HOL}
+\label{sec:isabelle}
 
-\todo{Explain Isabelle/jedit server interaction}
+\index{Isabelle proof assistant}
+
+\subsection{Installation}
+
+You need version Isabelle2013-2.
+
+\todo{put ... in ... etc/components}
+
+\subsection{Usage}
 
+\todo{Explain Isabelle/jedit server interaction}
 
 When using Isabelle, files generated from Why3 theories are stored in
 a dedicated XML format. Those files should not be edited. Instead,
-realizations must be designed in some \texttt{.thy} as follows. See
-directory \url{lib/isabelle} for examples.
+realizations must be designed in some \texttt{.thy} as follows. 
+
+\subsection{Realizations}
 
 The realization file corresponding to some Why3 file \url{f.why}
 should have the following form. 
@@ -29,3 +40,12 @@ why3_vc <some other lemma> by proof
 why3_end
 \end{verbatim}
 
+
+See directory \url{lib/isabelle} for examples.
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-PDF-mode: t
+%%% TeX-master: "manual"
+%%% End:
diff --git a/doc/itp.tex b/doc/itp.tex
index b7f6ea942658b7060e8cfd8110128f109827bf72..a2819f3a6ab6594db5691cce1e216fa29ffcacd5 100644
--- a/doc/itp.tex
+++ b/doc/itp.tex
@@ -5,6 +5,8 @@
 
 \todo{expliquer les principes}
 
+... We then provide specific information about some ITPs.
+
 \section{Theory Realizations}
 \label{sec:realizations}
 
@@ -99,11 +101,10 @@ This configuration file can be passed to \why thanks to the
 \index{driver@\verb+driver+}
 
 
-
-\section{Specific Information about some ITPs}
-
 \input{./coq.tex}
 
+\input{./coq_tactic.tex}
+
 \input{./isabelle.tex}
 
 \input{./pvs.tex}
diff --git a/doc/manual.tex b/doc/manual.tex
index cbc884620bf0e83db0644082ed2211a00ebf27b0..26afe8a88f7e9e6e7e7764c6a0d624cc3f1c8116 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -239,7 +239,6 @@ Thi-Minh-Tuyen Nguyen, Asma Tafat, Piotr Trojanek.
 
 \input{itp.tex}
 
-\input{coq_tactic.tex}
 
 % \chapter{Complete API documentation} *)
 % \label{chap:apidoc} *)
diff --git a/doc/pvs.tex b/doc/pvs.tex
index 4e6ab71f811604b92e7bd418c2cacf5eadd560d9..56a9f04693472f14c713e10580c60396db0dd71f 100644
--- a/doc/pvs.tex
+++ b/doc/pvs.tex
@@ -1,4 +1,13 @@
-\subsection{PVS}
+\section{PVS}
+\label{sec:pvs}
+
+\index{PVS proof assistant}
+
+\subsection{Installation}
+
+You need version 6.0.
+
+\subsection{Usage}
 
 When a PVS file is regenerated, the old version is split into chunks,
 according to blank lines. Chunks corresponding to \why declarations
@@ -13,6 +22,8 @@ otherwise, there will be two
 declarations for \texttt{f} in the next version of the file (one being
 regenerated and another one considered to be a user-edited chunk).
 
+\subsection{Realization}
+
 The user is allowed to perform the following actions on a PVS
 realization:
 \begin{itemize}
@@ -36,3 +47,10 @@ realization:
 \why makes some effort to merge new declarations with old ones
 and with user chunks. If it happens that some chunks could not be
 merged, they are appended at the end of the file, in comments.
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-PDF-mode: t
+%%% TeX-master: "manual"
+%%% End: