# HG changeset patch
# User blanchet
# Date 1303404442 -7200
# Node ID d105b1309a8d7b0fa9842829dc5834e0eca54b19
# Parent  c6ea64ebb8c5a079a3ba2cf24f9c2e117b8bd815
rewording

diff -r c6ea64ebb8c5 -r d105b1309a8d doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Thu Apr 21 18:39:22 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Thu Apr 21 18:47:22 2011 +0200
@@ -512,13 +512,13 @@
 \optrue{slicing}{no\_slicing}
 Specifies whether the time allocated to a prover should be sliced into several
 segments, each of which has its own set of possibly prover-dependent options.
-For SPASS and Vampire, the first slice tries the fast-but-incomplete
+For SPASS and Vampire, the first slice tries the fast but incomplete
 set-of-support (SOS) strategy, whereas the second slice runs without it. For E,
-up to three slices are defined, with different weighted search strategies and
+up to three slices are tried, with different weighted search strategies and
 number of facts. For SMT solvers, several slices are tried with the same options
-but fewer and fewer facts. According to benchmarks with a timeout of 30 seconds,
-slicing is a valuable optimization, and you should probably leave it enabled
-unless you are conducting experiments. However, this option is implicitly
+each time but fewer and fewer facts. According to benchmarks with a timeout of
+30 seconds, slicing is a valuable optimization, and you should probably leave it
+enabled unless you are conducting experiments. This option is implicitly
 disabled for (short) automatic runs.
 
 \nopagebreak