src/HOL/Library/ExecutableSet.thy

 | "unionl xs ys = foldr insertl xs ys"
 by pat_completeness auto
 termination by lexicographic_order
 
 lemmas unionl_def = unionl.simps(2)
-declare unionl.simps[code]
 
 function intersect :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where
   "intersect [] ys = []"
 | "intersect xs [] = []"
 | "intersect xs ys = filter (member xs) ys"
 by pat_completeness auto
 termination by lexicographic_order
 
 lemmas intersect_def = intersect.simps(3)
-declare intersect.simps[code]
 
 function subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where
   "subtract [] ys = ys"
 | "subtract xs [] = []"
 | "subtract xs ys = foldr remove1 xs ys"
 by pat_completeness auto
 termination by lexicographic_order
 
 lemmas subtract_def = subtract.simps(3)
-declare subtract.simps[code]
 
 function map_distinct :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
 where
   "map_distinct f [] = []"
 | "map_distinct f xs = foldr (insertl o f) xs []"
 by pat_completeness auto
 termination by lexicographic_order
 
 lemmas map_distinct_def = map_distinct.simps(2)
-declare map_distinct.simps[code]
 
 function unions :: "'a list list \<Rightarrow> 'a list"
 where
   "unions [] = []"
   "unions xs = foldr unionl xs []"
 by pat_completeness auto
 termination by lexicographic_order
 
 lemmas unions_def = unions.simps(2)
-declare unions.simps[code]
 
 consts intersects :: "'a list list \<Rightarrow> 'a list"
 primrec
   "intersects (x#xs) = foldr intersect xs x"