Fixed bug in consts_code section.
--- a/src/HOL/MicroJava/BV/BVExample.thy Wed Nov 27 17:07:05 2002 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy Wed Nov 27 17:11:38 2002 +0100
@@ -456,7 +456,7 @@
"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" ("(_ \\ _)")
+ "op -" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("(_ \\\\ _)")
lemma JVM_sup_unfold [code]:
"JVMType.sup S m n = lift2 (Opt.sup