src/HOLCF/UpperPD.thy
changeset 25925 3dc4acca4388
parent 25904 8161f137b0e9
child 26041 c2e15e65165f
     1.1 --- a/src/HOLCF/UpperPD.thy	Fri Jan 18 08:30:12 2008 +0100
     1.2 +++ b/src/HOLCF/UpperPD.thy	Fri Jan 18 20:22:07 2008 +0100
     1.3 @@ -346,7 +346,7 @@
     1.4   apply (rule iffI)
     1.5    apply (subgoal_tac
     1.6      "adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>(upper_unit\<cdot>z) \<or> f\<cdot>ys \<sqsubseteq> f\<cdot>(upper_unit\<cdot>z))")
     1.7 -   apply (drule admD [rule_format], rule chain_approx)
     1.8 +   apply (drule admD, rule chain_approx)
     1.9      apply (drule_tac f="approx i" in monofun_cfun_arg)
    1.10      apply (cut_tac xs="approx i\<cdot>xs" in compact_imp_upper_principal, simp)
    1.11      apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_upper_principal, simp)