src/HOL/ex/Set_Comprehension_Pointfree_Examples.thy
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