--- a/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy Sat Oct 20 09:09:35 2012 +0200
+++ b/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy Sat Oct 20 09:09:37 2012 +0200
@@ -125,6 +125,12 @@
where
"common_subsets S1 S2 = {S. S \<subseteq> S1 \<and> S \<subseteq> S2}"
-export_code union common_subsets in Haskell file -
+definition products :: "nat set => nat set => nat set"
+where
+ "products A B = {c. EX a b. a : A & b : B & c = a * b}"
+
+export_code products in Haskell file -
+
+export_code union common_subsets products in Haskell file -
end