src/HOLCF/LowerPD.thy

   "(lower_unit\<cdot>x \<sqsubseteq> lower_plus\<cdot>ys\<cdot>zs) =
     (lower_unit\<cdot>x \<sqsubseteq> ys \<or> lower_unit\<cdot>x \<sqsubseteq> zs)"
  apply (rule iffI)
   apply (subgoal_tac
     "adm (\<lambda>f. f\<cdot>(lower_unit\<cdot>x) \<sqsubseteq> f\<cdot>ys \<or> f\<cdot>(lower_unit\<cdot>x) \<sqsubseteq> f\<cdot>zs)")
-   apply (drule admD [rule_format], rule chain_approx)
+   apply (drule admD, rule chain_approx)
     apply (drule_tac f="approx i" in monofun_cfun_arg)
     apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
     apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_lower_principal, simp)
     apply (cut_tac xs="approx i\<cdot>zs" in compact_imp_lower_principal, simp)
     apply (clarify, simp add: lower_le_PDUnit_PDPlus_iff)