| changeset 11507 | 4b32a46ffd29 |
| parent 11499 | 7a7bb59a05db |
| child 11558 | 6539627881e8 |
--- a/src/HOL/NanoJava/State.thy Wed Aug 29 21:17:24 2001 +0200 +++ b/src/HOL/NanoJava/State.thy Thu Aug 30 15:47:30 2001 +0200 @@ -10,7 +10,7 @@ constdefs - body :: "imname => stmt" + body :: "cname \<times> mname => stmt" "body \<equiv> \<lambda>(C,m). bdy (the (method C m))" text {* locations, i.e.\ abstract references to objects *}