src/HOL/MicroJava/BV/LBVCorrect.thy

--- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Thu Jul 06 11:24:09 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Thu Jul 06 12:15:05 2000 +0200
@@ -138,9 +138,9 @@
   qed;  
   with all; 
   show ?thesis;  
-  proof elim; 
+  proof (elim exE allE impE conjE); 
     show "wtl_inst_list is G rT s0 s2 cert (0+length is) 0"; by simp; 
-  qed (auto simp add: fits_def); 
+  qed (auto simp add: fits_def);  
 qed;