diff options
| author | filliatr | 2001-04-06 12:18:05 +0000 |
|---|---|---|
| committer | filliatr | 2001-04-06 12:18:05 +0000 |
| commit | 48aff2bc219295950c032ba09b748f0690f5a2bc (patch) | |
| tree | 87ecaddb3c76b7f303424574eb7182ac797255cb | |
| parent | 7320f93631e5132a31299bac01b59eeb1d04ace5 (diff) | |
mise � jour V7
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8168 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rwxr-xr-x | doc/Omega.tex | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/Omega.tex b/doc/Omega.tex index 286c151c46..708e1f089c 100755 --- a/doc/Omega.tex +++ b/doc/Omega.tex @@ -50,7 +50,7 @@ on atomic formulas. Atomic formulas are built from the predicates and in expressions of type \verb=Z=, {\tt Omega}~recognizes \begin{quote} -\verb!+,_,*, Zs!, and constants. +\verb!+, -, *, Zs!, and constants. \end{quote} All expressions of type \verb=nat= or \verb=Z= not built on these @@ -142,7 +142,7 @@ Goal (z:Z)`z>0` -> `2*z + 1 > z`. Intro; Omega. \end{coq_example} -Other examples can be found in \verb+$COQLIB/theories/DEMOS/OMEGA+. +% Other examples can be found in \verb+$COQLIB/theories/DEMOS/OMEGA+. \asection{Technical data} \label{technical} @@ -209,7 +209,7 @@ decision procedure is only partial. \item Much too slow. -\item Certainely plenty other bugs !! You can report them to +\item Certainely other bugs! You can report them to \begin{quote} \verb=Pierre.Cregut@cnet.francetelecom.fr= |