equal
deleted
inserted
replaced
454 "image" ("map") |
454 "image" ("map") |
455 "UNION" ("(fn A => fn f => flat (map f A))") |
455 "UNION" ("(fn A => fn f => flat (map f A))") |
456 "Bex" ("(fn A => fn f => exists f A)") |
456 "Bex" ("(fn A => fn f => exists f A)") |
457 "Ball" ("(fn A => fn f => forall f A)") |
457 "Ball" ("(fn A => fn f => forall f A)") |
458 "some_elem" ("hd") |
458 "some_elem" ("hd") |
459 "op -" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("(_ \\ _)") |
459 "op -" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("(_ \\\\ _)") |
460 |
460 |
461 lemma JVM_sup_unfold [code]: |
461 lemma JVM_sup_unfold [code]: |
462 "JVMType.sup S m n = lift2 (Opt.sup |
462 "JVMType.sup S m n = lift2 (Opt.sup |
463 (Product.sup (Listn.sup (JType.sup S)) |
463 (Product.sup (Listn.sup (JType.sup S)) |
464 (\<lambda>x y. OK (map2 (lift2 (JType.sup S)) x y))))" |
464 (\<lambda>x y. OK (map2 (lift2 (JType.sup S)) x y))))" |