src/HOL/Library/Executable_Set.thy

 begin
 
 subsection {* Preprocessor setup *}
 
 declare member [code] 
+
+definition empty :: "'a set" where
+  "empty = {}"
+
+declare empty_def [symmetric, code_unfold]
+
+definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+  "inter = op \<inter>"
+
+declare inter_def [symmetric, code_unfold]
+
+definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+  "union = op \<union>"
+
+declare union_def [symmetric, code_unfold]
 
 definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   "subset = op \<le>"
 
 declare subset_def [symmetric, code_unfold]

 
 consts_code
   Set ("\<module>Set")
 
 consts_code
-  "Set.empty"         ("{*Fset.empty*}")
+  "empty"             ("{*Fset.empty*}")
   "List_Set.is_empty" ("{*Fset.is_empty*}")
   "Set.insert"        ("{*Fset.insert*}")
   "List_Set.remove"   ("{*Fset.remove*}")
   "Set.image"         ("{*Fset.map*}")
   "List_Set.project"  ("{*Fset.filter*}")
   "Ball"              ("{*flip Fset.forall*}")
   "Bex"               ("{*flip Fset.exists*}")
-  "op \<union>"              ("{*Fset.union*}")
-  "op \<inter>"              ("{*Fset.inter*}")
+  "union"             ("{*Fset.union*}")
+  "inter"             ("{*Fset.inter*}")
   "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip Fset.subtract*}")
   "Union"             ("{*Fset.Union*}")
   "Inter"             ("{*Fset.Inter*}")
   card                ("{*Fset.card*}")
   fold                ("{*foldl o flip*}")
 
-hide (open) const subset eq_set Inter Union flip
+hide (open) const empty inter union subset eq_set Inter Union flip
 
 end