# HG changeset patch
# User blanchet
# Date 1309179392 -7200
# Node ID cfb2077cb2dba62db351eed3de6013dff8cc2975
# Parent  940b714bd35ef6950c31e98a8344c1f5bd4ecc74
tweaked comment

diff -r 940b714bd35e -r cfb2077cb2db src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 27 14:56:31 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 27 14:56:32 2011 +0200
@@ -88,8 +88,8 @@
    time available given to the slice and should add up to 1.0. The "bool"
    component indicates whether the slice's strategy is complete; the "int", the
    preferred number of facts to pass; the first "string", the preferred type
-   system; the second "string", extra information to the prover (e.g., SOS or no
-   SOS).
+   system (which should be sound or quasi-sound); the second "string", extra
+   information to the prover (e.g., SOS or no SOS).
 
    The last slice should be the most "normal" one, because it will get all the
    time available if the other slices fail early and also because it is used if