src/HOL/MicroJava/BV/LBVComplete.thy

   show ?thesis
   proof (cases (open) "cert!pc")
     case None
     with wtl fits
     show ?thesis 
-      by - (rule wtl_inst_mono [elimify], (simp add: wtl_cert_def)+)
+      by - (rule wtl_inst_mono [elimified], (simp add: wtl_cert_def)+)
   next
     case Some
     with wtl fits
 
     have G: "G \<turnstile> s2 <=' (Some a)"

 
 lemma fits_imp_wtl_method_complete:
   "[| wt_method G C pTs rT mxl ins phi; fits ins cert phi |] ==> 
   wtl_method G C pTs rT mxl ins cert"
 by (simp add: wt_method_def wtl_method_def)
-   (rule wt_imp_wtl_inst_list [rulify, elimify], auto simp add: wt_start_def) 
+   (rule wt_imp_wtl_inst_list [rulified, elimified], auto simp add: wt_start_def) 
 
 
 lemma wtl_method_complete:
   "wt_method G C pTs rT mxl ins phi ==> 
   wtl_method G C pTs rT mxl ins (make_cert ins phi)"

     assume uG : "unique G" 
     assume b  : "((ac, ba), ad, ae, bb) \<in> set b"
 
     from 1
     show "wtl_method G a ba ad ae bb (make_Cert G Phi a (ac, ba))"
-    proof (rule bspec [elimify], clarsimp)
+    proof (rule bspec [elimified], clarsimp)
       assume ub : "unique b"
       assume m: "\<forall>(sig,rT,mb)\<in>set b. wf_mhead G sig rT \<and> 
                   (\<lambda>(maxl,b). wt_method G a (snd sig) rT maxl b (Phi a sig)) mb" 
       from m b
       show ?thesis
-      proof (rule bspec [elimify], clarsimp)
+      proof (rule bspec [elimified], clarsimp)
         assume "wt_method G a ba ad ae bb (Phi a (ac, ba))"         
         with wfprog uG ub b 1
         show ?thesis
-          by - (rule wtl_method_complete [elimify], assumption+, 
+          by - (rule wtl_method_complete [elimified], assumption+, 
                 simp add: make_Cert_def unique_epsilon)
       qed 
     qed
   qed
 qed