Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorblanchet
Sat, 07 Mar 2009 12:27:26 +0100
changeset 30348 5598523c482a
parent 30333 e9971af27b11 (current diff)
parent 30347 91f73b2997f9 (diff)
child 30349 110826d1e5ff
merged
--- a/src/HOL/Tools/refute.ML	Sat Mar 07 10:06:58 2009 +0100
+++ b/src/HOL/Tools/refute.ML	Sat Mar 07 12:27:26 2009 +0100
@@ -1227,7 +1227,7 @@
           SatSolver.SATISFIABLE assignment =>
           (Output.priority ("*** Model found: ***\n" ^ print_model thy model
             (fn i => case assignment i of SOME b => b | NONE => true));
-           "genuine")
+           if maybe_spurious then "potential" else "genuine")
         | SatSolver.UNSATISFIABLE _ =>
           (Output.priority "No model exists.";
           case next_universe universe sizes minsize maxsize of
isabelle