author | kleing |
Thu, 22 Feb 2001 11:47:35 +0100 | |
changeset 11177 | 749fd046002f |
parent 11176 | dec03152d163 |
child 11178 | 0a9d14823644 |
--- 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