make Quickcheck identify itself, so people don't submit bug reports to me thinking that it was Nitpick
authorblanchet
Tue, 09 Feb 2010 16:05:49 +0100
changeset 35077 c1dac8ace020
parent 35076 cc19e2aef17e
child 35078 6fd1052fe463
make Quickcheck identify itself, so people don't submit bug reports to me thinking that it was Nitpick
src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Fri Feb 05 14:27:21 2010 +0100
+++ b/src/Tools/quickcheck.ML	Tue Feb 09 16:05:49 2010 +0100
@@ -153,9 +153,9 @@
       |> ObjectLogic.atomize_term thy;
   in test_term ctxt quiet generator_name size iterations gi' end;
 
-fun pretty_counterex ctxt NONE = Pretty.str "No counterexamples found."
+fun pretty_counterex ctxt NONE = Pretty.str "Quickcheck found no counterexample."
   | pretty_counterex ctxt (SOME cex) =
-      Pretty.chunks (Pretty.str "Counterexample found:\n" ::
+      Pretty.chunks (Pretty.str "Quickcheck found a counterexample:\n" ::
         map (fn (s, t) =>
           Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) cex);