# HG changeset patch
# User berghofe
# Date 1127672129 -7200
# Node ID 1db9597176c8e04cb964e7c7101229c8d34f540f
# Parent  9234108fdfb1db3a2e6e5b07440fa72cd2b289a3
Now uses set implementation from ExecutableSet.

diff -r 9234108fdfb1 -r 1db9597176c8 src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Sun Sep 25 20:14:39 2005 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Sun Sep 25 20:15:29 2005 +0200
@@ -5,7 +5,7 @@
 
 header {* \isaheader{Example Welltypings}\label{sec:BVExample} *}
 
-theory BVExample imports JVMListExample BVSpecTypeSafe JVM begin
+theory BVExample imports JVMListExample BVSpecTypeSafe JVM ExecutableSet begin
 
 text {*
   This theory shows type correctness of the example program in section 
@@ -445,20 +445,8 @@
        (ss,w)"
   by (unfold iter_def some_elem_def, rule refl)
 
-types_code
-  set ("_ list")
-
 consts_code
-  "{}"     ("[]")
-  "insert" ("(_ ins _)")
-  "op :"   ("(_ mem _)")
-  "op Un"  ("(_ union _)")
-  "image"  ("map")
-  "UNION"  ("(fn A => fn f => List.concat (map f A))")
-  "Bex"    ("(fn A => fn f => exists f A)")
-  "Ball"   ("(fn A => fn f => forall f A)")
   "some_elem" ("hd")
-  "op -" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"  ("(_ \\\\ _)")
 
 lemma JVM_sup_unfold [code]:
  "JVMType.sup S m n = lift2 (Opt.sup