src/HOL/Library/Executable_Set.thy

   "unionl [] ys = ys"
 | "unionl xs ys = foldr insertl xs ys"
 by pat_completeness auto
 termination by lexicographic_order
 
-lemmas unionl_def = unionl.simps(2)
+lemmas unionl_eq = unionl.simps(2)
 
 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)
+lemmas intersect_eq = intersect.simps(3)
 
 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)
+lemmas subtract_eq = subtract.simps(3)
 
 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)
+lemmas map_distinct_eq = map_distinct.simps(2)
 
 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)
+lemmas unions_eq = unions.simps(2)
 
 consts intersects :: "'a list list \<Rightarrow> 'a list"
 primrec
   "intersects (x#xs) = foldr intersect xs x"
 

   shows "set (remove1 x xs) = set xs - {x}"
   using distnct set_remove1_eq by auto
 
 lemma iso_union:
   "set (unionl xs ys) = set xs \<union> set ys"
-  unfolding unionl_def
+  unfolding unionl_eq
   by (induct xs arbitrary: ys) (simp_all add: iso_insert)
 
 lemma iso_intersect:
   "set (intersect xs ys) = set xs \<inter> set ys"
-  unfolding intersect_def Int_def by (simp add: Int_def iso_member) auto
+  unfolding intersect_eq Int_def by (simp add: Int_def iso_member) auto
 
 definition
   subtract' :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   "subtract' = flip subtract"
 
 lemma iso_subtract:
   fixes ys
   assumes distnct: "distinct ys"
   shows "set (subtract' ys xs) = set ys - set xs"
     and "distinct (subtract' ys xs)"
-  unfolding subtract'_def flip_def subtract_def
+  unfolding subtract'_def flip_def subtract_eq
   using distnct by (induct xs arbitrary: ys) auto
 
 lemma iso_map_distinct:
   "set (map_distinct f xs) = image f (set xs)"
-  unfolding map_distinct_def by (induct xs) (simp_all add: iso_insert)
+  unfolding map_distinct_eq by (induct xs) (simp_all add: iso_insert)
 
 lemma iso_unions:
   "set (unions xss) = \<Union> set (map set xss)"
-  unfolding unions_def
+  unfolding unions_eq
 proof (induct xss)
   case Nil show ?case by simp
 next
   case (Cons xs xss) thus ?case by (induct xs) (simp_all add: iso_insert)
 qed