Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
changeset 61325 1cfc476198c9
parent 59433 9da5b2c61049
child 69593 3dda49e08b9d 
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Oct 05 15:57:25 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Oct 05 16:14:33 2015 +0200
@@ -787,8 +787,8 @@
              case polar of
                Neut =>
                if opt1 then raise NUT ("Nitpick_Kodkod.to_f (Finite)", [u])
-               else KK.True
-             | Pos => formula_for_bool (not opt1)
+               else KK.True (* sound? *)
+             | Pos => KK.False
              | Neg => KK.True
            end
          | Op1 (IsUnknown, _, _, u1) => kk_no (to_r u1)
isabelle