# HG changeset patch
# User bulwahn
# Date 1350716977 -7200
# Node ID 29cd291bfea6974a61e039c4461a5af496857901
# Parent  a69ec82ffae697f37a2d787a4cb24238db1cd696
adding another test case for the set_comprehension_simproc to the theory in HOL/ex

diff -r a69ec82ffae6 -r 29cd291bfea6 src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy
--- 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