equal
deleted
inserted
replaced
447 |
447 |
448 consts_code |
448 consts_code |
449 "some_elem" ("hd") |
449 "some_elem" ("hd") |
450 |
450 |
451 code_const some_elem |
451 code_const some_elem |
452 (SML target_atom "hd") |
452 (SML "hd") |
453 |
453 |
454 lemma JVM_sup_unfold [code]: |
454 lemma JVM_sup_unfold [code]: |
455 "JVMType.sup S m n = lift2 (Opt.sup |
455 "JVMType.sup S m n = lift2 (Opt.sup |
456 (Product.sup (Listn.sup (JType.sup S)) |
456 (Product.sup (Listn.sup (JType.sup S)) |
457 (\<lambda>x y. OK (map2 (lift2 (JType.sup S)) x y))))" |
457 (\<lambda>x y. OK (map2 (lift2 (JType.sup S)) x y))))" |