# HG changeset patch
# User haftmann
# Date 1246270736 -7200
# Node ID e81d0f04ffdf947c2ae5b1c25504bfbfa7fc3134
# Parent  431d8588bcad66b96cc6a32c3e85dd33f1cd1228
Executable_Set is now a simple wrapper around Fset

diff -r 431d8588bcad -r e81d0f04ffdf src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Mon Jun 29 12:18:55 2009 +0200
+++ b/src/HOL/Library/Executable_Set.thy	Mon Jun 29 12:18:56 2009 +0200
@@ -5,7 +5,7 @@
 header {* Implementation of finite sets by lists *}
 
 theory Executable_Set
-imports Main Code_Set
+imports Main Fset
 begin
 
 subsection {* Derived set operations *}
@@ -45,41 +45,39 @@
 
 subsection {* code generator setup *}
 
-text {* eliminate popular infixes *}
-
 ML {*
 nonfix inter;
 nonfix union;
 nonfix subset;
 *}
 
-text {* type @{typ "'a fset"} *}
-
-types_code
-  fset ("(_/ list)")
-
-consts_code
-  Set ("_")
-
-text {* primitive operations *}
-
 definition flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
   "flip f a b = f b a"
 
+types_code
+  fset ("(_/ \<module>fset)")
+attach {*
+datatype 'a fset = Set of 'a list;
+*}
+
 consts_code
-  "Set.empty"         ("{*Code_Set.empty*}")
-  "List_Set.is_empty" ("{*Code_Set.is_empty*}")
-  "Set.insert"        ("{*Code_Set.insert*}")
-  "List_Set.remove"   ("{*Code_Set.remove*}")
-  "Set.image"         ("{*Code_Set.map*}")
-  "List_Set.project"  ("{*Code_Set.filter*}")
-  "Ball"              ("{*flip Code_Set.forall*}")
-  "Bex"               ("{*flip Code_Set.exists*}")
-  "op \<union>"              ("{*Code_Set.union*}")
-  "op \<inter>"              ("{*Code_Set.inter*}")
-  "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip subtract*}")
-  "Set.Union"         ("{*Code_Set.union*}")
-  "Set.Inter"         ("{*Code_Set.inter*}")
+  Set ("\<module>Set")
+
+consts_code
+  "Set.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*}")
+  "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip Fset.subtract*}")
+  "Set.Union"         ("{*Fset.Union*}")
+  "Set.Inter"         ("{*Fset.Inter*}")
+  card                ("{*Fset.card*}")
   fold                ("{*foldl o flip*}")
 
 end
\ No newline at end of file