1.1 --- a/src/HOL/MicroJava/JVM/JVMState.thy	Thu Feb 22 11:31:31 2001 +0100
     1.2 +++ b/src/HOL/MicroJava/JVM/JVMState.thy	Thu Feb 22 11:47:35 2001 +0100
     1.3 @@ -40,10 +40,4 @@
     1.4  types
     1.5    jvm_state = "xcpt option \<times> aheap \<times> frame list"	
     1.6  
     1.7 -
     1.8 -text {* dynamic method lookup: *}
     1.9 -constdefs
    1.10 -  dyn_class	:: "'code prog \<times> sig \<times> cname => cname"
    1.11 -  "dyn_class == \<lambda>(G,sig,C). fst(the(method(G,C) sig))"
    1.12 -
    1.13  end