--- 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 \
--- 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
--- 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" ];
--- 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! *}