src/HOL/MicroJava/BV/Convert.thy

 
   thus ?thesis by blast
 qed
 
 
-theorem sup_loc_update [rulify]:
+theorem sup_loc_update [rulified]:
   "\<forall> n y. (G \<turnstile> a <=o b) \<longrightarrow> n < length y \<longrightarrow> (G \<turnstile> x <=l y) \<longrightarrow> 
           (G \<turnstile> x[n := a] <=l y[n := b])" (is "?P x")
 proof (induct x)
   show "?P []" by simp
 

     show "G \<turnstile> (a!n) <=o (c!n)" .
   qed
 
   with G
   show ?thesis 
-    by (auto intro!: all_nth_sup_loc [rulify] dest!: sup_loc_length) 
+    by (auto intro!: all_nth_sup_loc [rulified] dest!: sup_loc_length) 
 qed
   
 
 theorem sup_state_trans [trans]:
   "\<lbrakk>G \<turnstile> a <=s b; G \<turnstile> b <=s c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=s c"