changeset 13727 | 4ab8d49ab981 |
parent 13214 | 2aa33ed5f526 |
child 14045 | a34d89ce6097 |
--- 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