equal
deleted
inserted
replaced
41 | BODY pname |
41 | BODY pname |
42 | Call vname pname aexp ("_:=CALL _'(_')" [65, 65, 0] 60) |
42 | Call vname pname aexp ("_:=CALL _'(_')" [65, 65, 0] 60) |
43 |
43 |
44 consts bodies :: "(pname * com) list"(* finitely many procedure definitions *) |
44 consts bodies :: "(pname * com) list"(* finitely many procedure definitions *) |
45 definition |
45 definition |
46 body :: " pname ~=> com" where |
46 body :: " pname \<rightharpoonup> com" where |
47 "body = map_of bodies" |
47 "body = map_of bodies" |
48 |
48 |
49 |
49 |
50 (* Well-typedness: all procedures called must exist *) |
50 (* Well-typedness: all procedures called must exist *) |
51 |
51 |