--- a/src/HOL/MicroJava/BV/Correct.thy Thu Feb 22 11:47:35 2001 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy Thu Feb 22 18:03:11 2001 +0100
@@ -25,11 +25,6 @@
approx_stk G hp stk ST \<and> approx_loc G hp loc LT \<and>
pc < length ins \<and> length loc=length(snd sig)+maxl+1"
- correct_frame_opt :: "[jvm_prog,aheap,state_type option,nat,bytecode]
- => frame => bool"
- "correct_frame_opt G hp s ==
- case s of None => \<lambda>maxl ins f. False | Some t => correct_frame G hp t"
-
consts
correct_frames :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] => bool"