| changeset 11177 | 749fd046002f |
| parent 10922 | f1209aff9517 |
| child 12519 | a955fe2879ba |
--- a/src/HOL/MicroJava/JVM/JVMState.thy Thu Feb 22 11:31:31 2001 +0100 +++ b/src/HOL/MicroJava/JVM/JVMState.thy Thu Feb 22 11:47:35 2001 +0100 @@ -40,10 +40,4 @@ types jvm_state = "xcpt option \<times> aheap \<times> frame list" - -text {* dynamic method lookup: *} -constdefs - dyn_class :: "'code prog \<times> sig \<times> cname => cname" - "dyn_class == \<lambda>(G,sig,C). fst(the(method(G,C) sig))" - end