Commit bc4bba0c authored by Guillaume Melquiond's avatar Guillaume Melquiond

Slant i.e. and e.g. in documentation.

parent 690242b2
......@@ -52,7 +52,7 @@ It is also installable from sources, available from the site
\url{http://ocaml.info/home/ocaml_sources.html#ocaml-sqlite3}
\end{itemize}
If you want to use the specific Coq features, i.e the Coq
If you want to use the specific Coq features, \ie the Coq
tactic~\ref{chap:tactic} and Coq realizations~\ref{chap: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
......@@ -70,7 +70,7 @@ Installation can be tested as follows:
\begin{enumerate}
\item install some external provers (see~Section\ref{provers} below)
\item run \verb|why3config --detect|
\item run some examples from the distribution, \emph{e.g.} you should
\item run some examples from the distribution, \eg you should
obtain the following:
\begin{verbatim}
$ cd examples
......@@ -126,14 +126,14 @@ Section~\ref{sec:why3config}.
\section{Multiple Versions of the Same Prover}
Since version 0.72, \why is able to use several versions of the same
prover, e.g. it can use both CVC3 2.2 and CVC3 2.4.1 at the same time.
prover, \eg it can use both CVC3 2.2 and CVC3 2.4.1 at the same time.
The automatic detection of provers looks for typical names for their
executable command, e.g. \texttt{cvc3} for CVC3. However, if you
executable command, \eg \texttt{cvc3} for CVC3. However, if you
install several version of the same prover it is likely that you would
use specialized executable names, such as \texttt{cvc3-2.2} or
\texttt{cvc3-2.4.1}. To allow the \why detection process to recognize
these, you can use the option \verb|--add-prover| to
\texttt{why3config}, e.g.
\texttt{why3config}, \eg
\begin{verbatim}
why3config --detect --add-prover cvc3-2.4 /usr/local/bin/cvc3-2.4.1
\end{verbatim}
......@@ -146,7 +146,7 @@ Appendix~\ref{sec:proverdetecttiondata} for details.
\section{Session Update after Prover Upgrade}
\label{sec:uninstalledprovers}
If you happen to upgrade a prover, e.g. installing CVC3 2.4.1 in place
If you happen to upgrade a prover, \eg installing CVC3 2.4.1 in place
of CVC3 2.2, then the proof sessions formerly recorded will still
refer to the old version of the prover. If you open one such a session
with the GUI, and replay the proofs, you will be asked to choose
......
......@@ -4,6 +4,7 @@
\newcommand{\why}{\textsf{Why3}\xspace}
\newcommand{\whyml}{\textsf{Why3ML}\xspace}
\newcommand{\eg}{\emph{e.g.}\xspace}
\newcommand{\ie}{\emph{i.e.}\xspace}
% BNF grammar
\newcommand{\keyword}[1]{\texttt{#1}}
......
......@@ -9,7 +9,7 @@ provided by the \why environment. These are as follows:
\item[\texttt{why3}] reads \why input files and call provers, on the command-line
\item[\texttt{why3ide}] graphical interface to display goals, run
provers and transformations on them.
\item[\texttt{why3ml}] as \texttt{why3} but reads \why{} ML programs instead
\item[\texttt{why3ml}] as \texttt{why3} but reads \whyml programs instead
\item[\texttt{why3replayer}] replay the proofs stored in a session,
for regression test purposes
\item[\texttt{why3bench}] produces benchmarks.
......@@ -134,8 +134,8 @@ The \texttt{why3} tool executes the following steps:
transformations, plugins can add more of them.
\item Apply the driver selected with the \verb|-D/--driver| option,
or the driver of the prover selected with \verb|-P/--prover|
option. \verb|--list-provers| lists the known provers, i.e.~the ones
which appear in the configuration file.
option. \verb|--list-provers| lists the known provers, \ie the ones
that appear in the configuration file.
\item If the option \verb|-P/--prover| is given, call the selected prover
on each generated task and print the results. If the option
\verb|-D/--driver| is given, print each generated task using
......@@ -274,7 +274,7 @@ are groups together under several tabs
\begin{itemize}
\item introduce premises: if selected, the goal of the task shownin
top-right window is displayed after introduction of universally
quantified variables and implications, e.g. a goal of the form
quantified variables and implications, \eg a goal of the form
$\forall x: t. P \rightarrow Q$ is displayed as
\[
\begin{array}{l}
......
......@@ -138,7 +138,7 @@ why3 --list-transforms
definitions~\cite{paskevich09rr}
\item[eliminate\_builtin] Suppress definitions of symbols which are
declared as builtin in the driver, i.e. with a ``syntax'' rule.
declared as builtin in the driver, \ie with a ``syntax'' rule.
\item[eliminate\_definition\_func]
Replaces all function definitions with axioms.
\item[eliminate\_definition\_pred]
......@@ -162,7 +162,7 @@ definitions~\cite{paskevich09rr}
Apply both transformations above.
\item[eliminate\_inductive] replaces inductive predicates by
(incomplete) axiomatic definitions, i.e. construction axioms and
(incomplete) axiomatic definitions, \ie construction axioms and
an inversion axiom.
\item[eliminate\_let\_fmla]
......@@ -223,7 +223,7 @@ each $x_1$ .. $x_n$ occur at most once in the $e_i$
and f'' to ``f'', etc.
\item[simplify\_recursive\_definition] reduces mutually recursive
definitions if they are not really mutually recursive, e.g.:
definitions if they are not really mutually recursive, \eg
\begin{verbatim}
function f : ... = .... g ...
......
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