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 35074c1dac8ace020
parent 35073 cc19e2aef17e
child 35075 6fd1052fe463
make Quickcheck identify itself, so people don't submit bug reports to me thinking that it was Nitpick
src/Tools/quickcheck.ML
     1.1 --- a/src/Tools/quickcheck.ML	Fri Feb 05 14:27:21 2010 +0100
     1.2 +++ b/src/Tools/quickcheck.ML	Tue Feb 09 16:05:49 2010 +0100
     1.3 @@ -153,9 +153,9 @@
     1.4        |> ObjectLogic.atomize_term thy;
     1.5    in test_term ctxt quiet generator_name size iterations gi' end;
     1.6  
     1.7 -fun pretty_counterex ctxt NONE = Pretty.str "No counterexamples found."
     1.8 +fun pretty_counterex ctxt NONE = Pretty.str "Quickcheck found no counterexample."
     1.9    | pretty_counterex ctxt (SOME cex) =
    1.10 -      Pretty.chunks (Pretty.str "Counterexample found:\n" ::
    1.11 +      Pretty.chunks (Pretty.str "Quickcheck found a counterexample:\n" ::
    1.12          map (fn (s, t) =>
    1.13            Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) cex);
    1.14