dropped Executable_Set wrapper theory
authorhaftmann
Mon Dec 26 17:40:43 2011 +0100 (2011-12-26)
changeset 459852d399a776de2
parent 45984 5de99514fd07
child 45986 c9e50153e5ae
dropped Executable_Set wrapper theory
src/HOL/IsaMakefile
src/HOL/Library/Executable_Set.thy
src/HOL/Library/ROOT.ML
src/HOL/MicroJava/BV/BVExample.thy
     1.1 --- a/src/HOL/IsaMakefile	Sun Dec 25 08:42:33 2011 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Mon Dec 26 17:40:43 2011 +0100
     1.3 @@ -447,7 +447,7 @@
     1.4    Library/Cset.thy Library/Cset_Monad.thy Library/Continuity.thy	\
     1.5    Library/Convex.thy Library/Countable.thy				\
     1.6    Library/Dlist.thy Library/Dlist_Cset.thy Library/Efficient_Nat.thy	\
     1.7 -  Library/Eval_Witness.thy Library/Executable_Set.thy			\
     1.8 +  Library/Eval_Witness.thy						\
     1.9    Library/Extended_Real.thy Library/Extended_Nat.thy Library/Float.thy	\
    1.10    Library/Formal_Power_Series.thy Library/Fraction_Field.thy		\
    1.11    Library/FrechetDeriv.thy Library/Cset.thy Library/FuncSet.thy		\
    1.12 @@ -963,7 +963,7 @@
    1.13  
    1.14  HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz
    1.15  
    1.16 -$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL Library/Executable_Set.thy		\
    1.17 +$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL					\
    1.18    MicroJava/ROOT.ML MicroJava/Comp/AuxLemmas.thy			\
    1.19    MicroJava/Comp/CorrComp.thy MicroJava/Comp/CorrCompTp.thy		\
    1.20    MicroJava/Comp/DefsComp.thy MicroJava/Comp/Index.thy			\
     2.1 --- a/src/HOL/Library/Executable_Set.thy	Sun Dec 25 08:42:33 2011 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,18 +0,0 @@
     2.4 -(*  Title:      HOL/Library/Executable_Set.thy
     2.5 -    Author:     Stefan Berghofer, TU Muenchen
     2.6 -    Author:     Florian Haftmann, TU Muenchen
     2.7 -*)
     2.8 -
     2.9 -header {* A thin compatibility layer *}
    2.10 -
    2.11 -theory Executable_Set
    2.12 -imports More_Set
    2.13 -begin
    2.14 -
    2.15 -abbreviation Set :: "'a list \<Rightarrow> 'a set" where
    2.16 -  "Set \<equiv> set"
    2.17 -
    2.18 -abbreviation Coset :: "'a list \<Rightarrow> 'a set" where
    2.19 -  "Coset \<equiv> More_Set.coset"
    2.20 -
    2.21 -end
     3.1 --- a/src/HOL/Library/ROOT.ML	Sun Dec 25 08:42:33 2011 +0100
     3.2 +++ b/src/HOL/Library/ROOT.ML	Mon Dec 26 17:40:43 2011 +0100
     3.3 @@ -3,5 +3,5 @@
     3.4  
     3.5  use_thys ["Library", "List_Cset", "List_Prefix", "List_lexord", "Sublist_Order",
     3.6    "Product_Lattice",
     3.7 -  "Code_Char_chr", "Code_Char_ord", "Code_Integer", "Efficient_Nat", "Executable_Set"(*, "Code_Prolog"*),
     3.8 +  "Code_Char_chr", "Code_Char_ord", "Code_Integer", "Efficient_Nat"(*, "Code_Prolog"*),
     3.9    "Code_Real_Approx_By_Float" ];
     4.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Sun Dec 25 08:42:33 2011 +0100
     4.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Mon Dec 26 17:40:43 2011 +0100
     4.3 @@ -9,7 +9,7 @@
     4.4    "../JVM/JVMListExample"
     4.5    BVSpecTypeSafe
     4.6    JVM
     4.7 -  "~~/src/HOL/Library/Executable_Set"
     4.8 +  "~~/src/HOL/Library/More_Set"
     4.9  begin
    4.10  
    4.11  text {*
    4.12 @@ -437,7 +437,6 @@
    4.13    "some_elem = (%S. SOME x. x : S)"
    4.14  code_const some_elem
    4.15    (SML "(case/ _ of/ Set/ xs/ =>/ hd/ xs)")
    4.16 -setup {* Code.add_signature_cmd ("some_elem", "'a set \<Rightarrow> 'a") *}
    4.17  
    4.18  text {* This code setup is just a demonstration and \emph{not} sound! *}
    4.19