src/HOLCF/Fix.thy

 
 subsection {* Fixed point induction *}
 
 lemma fix_ind: "\<lbrakk>adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P (fix\<cdot>F)"
 apply (subst fix_def2)
-apply (erule admD [rule_format])
+apply (erule admD)
 apply (rule chain_iterate)
 apply (induct_tac "i", simp_all)
 done
 
 lemma def_fix_ind:

 lemma adm_impl_admw: "adm P \<Longrightarrow> admw P"
 apply (unfold admw_def)
 apply (intro strip)
 apply (erule admD)
 apply (rule chain_iterate)
-apply assumption
+apply (erule spec)
 done
 
 text {* computational induction for weak admissible formulae *}
 
 lemma wfix_ind: "\<lbrakk>admw P; \<forall>n. P (iterate n\<cdot>F\<cdot>\<bottom>)\<rbrakk> \<Longrightarrow> P (fix\<cdot>F)"