src/HOL/Library/Executable_Set.thy

--- a/src/HOL/Library/Executable_Set.thy	Wed Sep 23 11:33:52 2009 +0200
+++ b/src/HOL/Library/Executable_Set.thy	Wed Sep 23 11:34:21 2009 +0200
@@ -12,6 +12,21 @@
 
 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>"
 
@@ -69,7 +84,7 @@
   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*}")
@@ -77,8 +92,8 @@
   "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*}")