changeset 69624 | e02bdf853a4c |
parent 67613 | ce654b0e6d69 |
--- a/src/HOL/ex/Set_Comprehension_Pointfree_Examples.thy Thu Jan 10 12:07:05 2019 +0000 +++ b/src/HOL/ex/Set_Comprehension_Pointfree_Examples.thy Thu Jan 10 12:07:08 2019 +0000 @@ -133,8 +133,6 @@ where "products A B = {c. \<exists>a b. a \<in> A \<and> b \<in> B \<and> c = a * b}" -export_code products in Haskell - -export_code union common_subsets products in Haskell +export_code union common_subsets products checking SML end