diff -r 9550a6f4ed4a -r 4ab8d49ab981 src/HOL/MicroJava/BV/BVExample.thy --- 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 \ 'a set \ 'a set" ("(_ \\ _)") + "op -" :: "'a set \ 'a set \ 'a set" ("(_ \\\\ _)") lemma JVM_sup_unfold [code]: "JVMType.sup S m n = lift2 (Opt.sup