src/HOL/Set.thy

   where "{} \<equiv> bot"
 
 definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set"
   where insert_compr: "insert a B = {x. x = a \<or> x \<in> B}"
 
+open_bundle set_enumeration_syntax
+begin
+
 syntax
   "_Finset" :: "args \<Rightarrow> 'a set"  (\<open>(\<open>indent=1 notation=\<open>mixfix set enumeration\<close>\<close>{_})\<close>)
 syntax_consts
   "_Finset" \<rightleftharpoons> insert
 translations
   "{x, xs}" \<rightleftharpoons> "CONST insert x {xs}"
   "{x}" \<rightleftharpoons> "CONST insert x {}"
+
+end
 
 
 subsection \<open>Subsets and bounded quantifiers\<close>
 
 abbreviation subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"