src/HOLCF/Adm.thy

 lemma adm_disj_lemma3: 
   "\<lbrakk>chain (Y::nat \<Rightarrow> 'a::cpo); \<forall>i. \<exists>j\<ge>i. P (Y j)\<rbrakk> \<Longrightarrow> 
     (\<Squnion>i. Y i) = (\<Squnion>i. Y (LEAST j. i \<le> j \<and> P (Y j)))"
  apply (frule (1) adm_disj_lemma1)
  apply (rule antisym_less)
-  apply (rule lub_mono [rule_format], assumption+)
+  apply (rule lub_mono, assumption+)
   apply (erule chain_mono)
   apply (simp add: adm_disj_lemma2)
  apply (rule lub_range_mono, fast, assumption+)
 done
 

 apply (rule admI)
 apply (simp add: cont2contlubE)
 apply (rule lub_mono)
 apply (erule (1) ch2ch_cont)
 apply (erule (1) ch2ch_cont)
-apply assumption
+apply (erule spec)
 done
 
 lemma adm_eq: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x = v x)"
 by (simp add: po_eq_conv adm_conj adm_less)