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.
improved values command to handle a special case with tuples and polymorphic predicates more correctly
authorbulwahn
Wed, 19 May 2010 18:24:04 +0200
changeset 37002 34e73e8bab66
parent 37001 bcffdb899167
child 37003 a393a588b82e
improved values command to handle a special case with tuples and polymorphic predicates more correctly
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed May 19 18:24:03 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed May 19 18:24:04 2010 +0200
@@ -3124,6 +3124,10 @@
                   instance_of (m1, Input) andalso instance_of (m2, Input)
               | instance_of (Pair (m1, m2), Output) =
                   instance_of (m1, Output) andalso instance_of (m2, Output)
+              | instance_of (Input, Pair (m1, m2)) =
+                  instance_of (Input, m1) andalso instance_of (Input, m2)
+              | instance_of (Output, Pair (m1, m2)) =
+                  instance_of (Output, m1) andalso instance_of (Output, m2)
               | instance_of _ = false
           in forall instance_of (strip_fun_mode m1 ~~ strip_fun_mode m2) end
         val derivs = all_derivations_of thy (all_modes_of thy) [] body
isabelle