removed unused function
authorkleing
Thu, 22 Feb 2001 11:47:35 +0100
changeset 11177 749fd046002f
parent 11176 dec03152d163
child 11178 0a9d14823644
removed unused function
src/HOL/MicroJava/JVM/JVMState.thy
--- 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