# HG changeset patch
# User blanchet
# Date 1416828913 -3600
# Node ID 3a215367670588fafc3c771cf6c2f3fa2e995469
# Parent  c5cfead18464f4a259e74cc66ca8b4d5903fa00e
renamed 'veriT' to 'verit', to stick to all-lowercase rule for prover names

diff -r c5cfead18464 -r 3a2153676705 src/Doc/Sledgehammer/document/root.tex
--- 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
diff -r c5cfead18464 -r 3a2153676705 src/HOL/SMT.thy
--- 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 {*
diff -r c5cfead18464 -r 3a2153676705 src/HOL/Tools/SMT/smt_systems.ML
--- 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",