renamed 'veriT' to 'verit', to stick to all-lowercase rule for prover names
authorblanchet
Mon Nov 24 12:35:13 2014 +0100 (2014-11-24)
changeset 590353a2153676705
parent 59034 c5cfead18464
child 59036 ce58eb744e38
renamed 'veriT' to 'verit', to stick to all-lowercase rule for prover names
src/Doc/Sledgehammer/document/root.tex
src/HOL/SMT.thy
src/HOL/Tools/SMT/smt_systems.ML
     1.1 --- a/src/Doc/Sledgehammer/document/root.tex	Mon Nov 24 12:35:13 2014 +0100
     1.2 +++ b/src/Doc/Sledgehammer/document/root.tex	Mon Nov 24 12:35:13 2014 +0100
     1.3 @@ -857,7 +857,7 @@
     1.4  ``3.0''). Sledgehammer has been tested with versions 0.6 to 3.0.
     1.5  Versions strictly above 1.8 support the TPTP typed first-order format (TFF0).
     1.6  
     1.7 -\item[\labelitemi] \textbf{\textit{veriT}:} veriT \cite{bouton-et-al-2009} is an
     1.8 +\item[\labelitemi] \textbf{\textit{verit}:} veriT \cite{bouton-et-al-2009} is an
     1.9  SMT solver developed by David Déharbe, Pascal Fontaine, and their colleagues.
    1.10  It is specifically designed to produce detailed proofs for reconstruction in
    1.11  proof assistants. To use veriT, set the environment variable
     2.1 --- a/src/HOL/SMT.thy	Mon Nov 24 12:35:13 2014 +0100
     2.2 +++ b/src/HOL/SMT.thy	Mon Nov 24 12:35:13 2014 +0100
     2.3 @@ -231,7 +231,7 @@
     2.4  
     2.5  declare [[cvc3_options = ""]]
     2.6  declare [[cvc4_options = "--full-saturate-quant --inst-when=full-last-call"]]
     2.7 -declare [[veriT_options = ""]]
     2.8 +declare [[verit_options = ""]]
     2.9  declare [[z3_options = ""]]
    2.10  
    2.11  text {*
     3.1 --- a/src/HOL/Tools/SMT/smt_systems.ML	Mon Nov 24 12:35:13 2014 +0100
     3.2 +++ b/src/HOL/Tools/SMT/smt_systems.ML	Mon Nov 24 12:35:13 2014 +0100
     3.3 @@ -96,7 +96,7 @@
     3.4  (* veriT *)
     3.5  
     3.6  val veriT: SMT_Solver.solver_config = {
     3.7 -  name = "veriT",
     3.8 +  name = "verit",
     3.9    class = K SMTLIB_Interface.smtlibC,
    3.10    avail = make_avail "VERIT",
    3.11    command = make_command "VERIT",