equal
deleted
inserted
replaced
167 |
167 |
168 text {* for compatibility with old HOLCF-Version *} |
168 text {* for compatibility with old HOLCF-Version *} |
169 lemma inst_up_pcpo: "\<bottom> = Ibottom" |
169 lemma inst_up_pcpo: "\<bottom> = Ibottom" |
170 by (rule minimal_up [THEN UU_I, symmetric]) |
170 by (rule minimal_up [THEN UU_I, symmetric]) |
171 |
171 |
172 subsection {* Continuity of @{term Iup} and @{term Ifup} *} |
172 subsection {* Continuity of \emph{Iup} and \emph{Ifup} *} |
173 |
173 |
174 text {* continuity for @{term Iup} *} |
174 text {* continuity for @{term Iup} *} |
175 |
175 |
176 lemma cont_Iup: "cont Iup" |
176 lemma cont_Iup: "cont Iup" |
177 apply (rule contI) |
177 apply (rule contI) |