adding another test case for the set_comprehension_simproc to the theory in HOL/ex
authorbulwahn
Sat, 20 Oct 2012 09:09:37 +0200
changeset 49947 29cd291bfea6
parent 49946 a69ec82ffae6
child 49948 744934b818c7
adding another test case for the set_comprehension_simproc to the theory in HOL/ex
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