src/HOL/ex/Set_Comprehension_Pointfree_Examples.thy
changeset 69624 e02bdf853a4c
parent 67613 ce654b0e6d69
equal deleted inserted replaced
69623:ef02c5e051e5 69624:e02bdf853a4c
   131 
   131 
   132 definition products :: "nat set => nat set => nat set"
   132 definition products :: "nat set => nat set => nat set"
   133 where
   133 where
   134   "products A B = {c. \<exists>a b. a \<in> A \<and> b \<in> B \<and> c = a * b}"
   134   "products A B = {c. \<exists>a b. a \<in> A \<and> b \<in> B \<and> c = a * b}"
   135 
   135 
   136 export_code products in Haskell
   136 export_code union common_subsets products checking SML
   137 
       
   138 export_code union common_subsets products in Haskell
       
   139 
   137 
   140 end
   138 end