--- a/src/Doc/Sledgehammer/document/root.tex Mon Nov 24 12:35:13 2014 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Mon Nov 24 12:35:13 2014 +0100
@@ -857,7 +857,7 @@
``3.0''). Sledgehammer has been tested with versions 0.6 to 3.0.
Versions strictly above 1.8 support the TPTP typed first-order format (TFF0).
-\item[\labelitemi] \textbf{\textit{veriT}:} veriT \cite{bouton-et-al-2009} is an
+\item[\labelitemi] \textbf{\textit{verit}:} veriT \cite{bouton-et-al-2009} is an
SMT solver developed by David Déharbe, Pascal Fontaine, and their colleagues.
It is specifically designed to produce detailed proofs for reconstruction in
proof assistants. To use veriT, set the environment variable
--- a/src/HOL/SMT.thy Mon Nov 24 12:35:13 2014 +0100
+++ b/src/HOL/SMT.thy Mon Nov 24 12:35:13 2014 +0100
@@ -231,7 +231,7 @@
declare [[cvc3_options = ""]]
declare [[cvc4_options = "--full-saturate-quant --inst-when=full-last-call"]]
-declare [[veriT_options = ""]]
+declare [[verit_options = ""]]
declare [[z3_options = ""]]
text {*
--- a/src/HOL/Tools/SMT/smt_systems.ML Mon Nov 24 12:35:13 2014 +0100
+++ b/src/HOL/Tools/SMT/smt_systems.ML Mon Nov 24 12:35:13 2014 +0100
@@ -96,7 +96,7 @@
(* veriT *)
val veriT: SMT_Solver.solver_config = {
- name = "veriT",
+ name = "verit",
class = K SMTLIB_Interface.smtlibC,
avail = make_avail "VERIT",
command = make_command "VERIT",