# HG changeset patch
# User haftmann
# Date 1324917643 -3600
# Node ID 2d399a776de28d3508d6eb8fa23e79fa40360e79
# Parent  5de99514fd07a75ced0d8c0ed8f8962e9dc0c368
dropped Executable_Set wrapper theory

diff -r 5de99514fd07 -r 2d399a776de2 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sun Dec 25 08:42:33 2011 +0100
+++ b/src/HOL/IsaMakefile	Mon Dec 26 17:40:43 2011 +0100
@@ -447,7 +447,7 @@
   Library/Cset.thy Library/Cset_Monad.thy Library/Continuity.thy	\
   Library/Convex.thy Library/Countable.thy				\
   Library/Dlist.thy Library/Dlist_Cset.thy Library/Efficient_Nat.thy	\
-  Library/Eval_Witness.thy Library/Executable_Set.thy			\
+  Library/Eval_Witness.thy						\
   Library/Extended_Real.thy Library/Extended_Nat.thy Library/Float.thy	\
   Library/Formal_Power_Series.thy Library/Fraction_Field.thy		\
   Library/FrechetDeriv.thy Library/Cset.thy Library/FuncSet.thy		\
@@ -963,7 +963,7 @@
 
 HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz
 
-$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL Library/Executable_Set.thy		\
+$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL					\
   MicroJava/ROOT.ML MicroJava/Comp/AuxLemmas.thy			\
   MicroJava/Comp/CorrComp.thy MicroJava/Comp/CorrCompTp.thy		\
   MicroJava/Comp/DefsComp.thy MicroJava/Comp/Index.thy			\
diff -r 5de99514fd07 -r 2d399a776de2 src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Sun Dec 25 08:42:33 2011 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-(*  Title:      HOL/Library/Executable_Set.thy
-    Author:     Stefan Berghofer, TU Muenchen
-    Author:     Florian Haftmann, TU Muenchen
-*)
-
-header {* A thin compatibility layer *}
-
-theory Executable_Set
-imports More_Set
-begin
-
-abbreviation Set :: "'a list \<Rightarrow> 'a set" where
-  "Set \<equiv> set"
-
-abbreviation Coset :: "'a list \<Rightarrow> 'a set" where
-  "Coset \<equiv> More_Set.coset"
-
-end
diff -r 5de99514fd07 -r 2d399a776de2 src/HOL/Library/ROOT.ML
--- a/src/HOL/Library/ROOT.ML	Sun Dec 25 08:42:33 2011 +0100
+++ b/src/HOL/Library/ROOT.ML	Mon Dec 26 17:40:43 2011 +0100
@@ -3,5 +3,5 @@
 
 use_thys ["Library", "List_Cset", "List_Prefix", "List_lexord", "Sublist_Order",
   "Product_Lattice",
-  "Code_Char_chr", "Code_Char_ord", "Code_Integer", "Efficient_Nat", "Executable_Set"(*, "Code_Prolog"*),
+  "Code_Char_chr", "Code_Char_ord", "Code_Integer", "Efficient_Nat"(*, "Code_Prolog"*),
   "Code_Real_Approx_By_Float" ];
diff -r 5de99514fd07 -r 2d399a776de2 src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Sun Dec 25 08:42:33 2011 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Mon Dec 26 17:40:43 2011 +0100
@@ -9,7 +9,7 @@
   "../JVM/JVMListExample"
   BVSpecTypeSafe
   JVM
-  "~~/src/HOL/Library/Executable_Set"
+  "~~/src/HOL/Library/More_Set"
 begin
 
 text {*
@@ -437,7 +437,6 @@
   "some_elem = (%S. SOME x. x : S)"
 code_const some_elem
   (SML "(case/ _ of/ Set/ xs/ =>/ hd/ xs)")
-setup {* Code.add_signature_cmd ("some_elem", "'a set \<Rightarrow> 'a") *}
 
 text {* This code setup is just a demonstration and \emph{not} sound! *}