# HG changeset patch # User blanchet # Date 1632734396 -7200 # Node ID ba30067b7259630f48c1d615ed4caa6feac8ec05 # Parent d1185d02aef5ca0ca86c05b6adfecbe4df837267 tuned docs diff -r d1185d02aef5 -r ba30067b7259 src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Sun Sep 26 20:13:28 2021 +0200 +++ b/src/Doc/Sledgehammer/document/root.tex Mon Sep 27 11:19:56 2021 +0200 @@ -235,13 +235,13 @@ % ``\textit{z3\/}'': Try this: \textbf{by} \textit{simp} (0.5 ms) \\ % -``\textit{spass\/}'': Try this: \textbf{by} \textit{simp} (0.3 ms) +``\textit{vampire\/}'': Try this: \textbf{by} \textit{simp} (0.3 ms) % \postw -Sledgehammer ran CVC4, E, SPASS, and Z3 in parallel. Depending on which -provers are installed and how many processor cores are available, some of the -provers might be missing or present with a \textit{remote\_} prefix. +Sledgehammer ran CVC4, E, Vampire, and Z3 in parallel. This list may vary +depending on which provers are installed and how many processor cores are +available. For each successful prover, Sledgehammer gives a one-line Isabelle proof. Rough timings are shown in parentheses, indicating how fast the call is. You can