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.
produce more potential counterexamples for subset operator (cf. quantifiers)
authorblanchet
Fri, 14 May 2010 12:01:16 +0200
changeset 36912 55b97cb3806e
parent 36911 0e2818493775
child 36913 0010f08e288e
produce more potential counterexamples for subset operator (cf. quantifiers)
src/HOL/Tools/Nitpick/nitpick_nut.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Fri May 14 11:24:49 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Fri May 14 12:01:16 2010 +0200
@@ -970,11 +970,11 @@
           in
             if is_opt_rep R then
               triad_fn (fn polar => s_op2 Subset T (Formula polar) u1 u2)
-            else if opt andalso polar = Pos andalso
-                    not (is_concrete_type datatypes true (type_of u1)) then
+            else if not opt orelse unsound orelse polar = Neg orelse
+                    is_concrete_type datatypes true (type_of u1) then
+              s_op2 Subset T R u1 u2
+            else
               Cst (False, T, Formula Pos)
-            else
-              s_op2 Subset T R u1 u2
           end
         | Op2 (DefEq, T, _, u1, u2) =>
           s_op2 DefEq T (Formula Neut) (sub u1) (sub u2)
isabelle