# HG changeset patch
# User blanchet
# Date 1390208827 -3600
# Node ID 3abfa9409ae40372db7263599143003aaea7b6b5
# Parent  de68c9c3e4549839d7f500d002e444e26de6f1d3
killed obsolete provers from documentation

diff -r de68c9c3e454 -r 3abfa9409ae4 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Sun Jan 19 23:02:00 2014 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Mon Jan 20 10:07:07 2014 +0100
@@ -923,10 +923,6 @@
 \item[\labelitemi] \textbf{\textit{remote\_agsyhol}:} The remote version of
 agsyHOL runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
 
-\item[\labelitemi] \textbf{\textit{remote\_cvc3}:} The remote version of CVC3 runs
-on servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
-point).
-
 \item[\labelitemi] \textbf{\textit{remote\_e}:} The remote version of E runs
 on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
 
@@ -971,10 +967,6 @@
 used to prove universally quantified equations using unconditional equations,
 corresponding to the TPTP CNF UEQ division. The remote version of Waldmeister
 runs on Geoff Sutcliffe's Miami servers.
-
-\item[\labelitemi] \textbf{\textit{remote\_z3}:} The remote version of Z3 runs on
-servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
-point).
 \end{enum}
 
 By default, Sledgehammer runs a selection of CVC3, E, E-SInE, SPASS, Vampire,