src/HOL/Library/ExecutableSet.thy

 
 definition
   insertl :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   "insertl x xs = (if member xs x then xs else x#xs)"
 
-lemma
-  [code target: List]: "member [] y \<longleftrightarrow> False"
+lemma [code target: List]: "member [] y \<longleftrightarrow> False"
   and [code target: List]: "member (x#xs) y \<longleftrightarrow> y = x \<or> member xs y"
-unfolding member_def by (induct xs) simp_all
+  unfolding member_def by (induct xs) simp_all
 
 fun
   drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   "drop_first f [] = []"
 | "drop_first f (x#xs) = (if f x then xs else x # drop_first f xs)"

 
 lemma iso_subtract:
   fixes ys
   assumes distnct: "distinct ys"
   shows "set (subtract' ys xs) = set ys - set xs"
-  and "distinct (subtract' ys xs)"
+    and "distinct (subtract' ys xs)"
   unfolding subtract'_def flip_def subtract_def
   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)
 
 lemma iso_unions:
   "set (unions xss) = \<Union> set (map set xss)"
-unfolding unions_def proof (induct xss)
+  unfolding unions_def
+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