equal
deleted
inserted
replaced
134 |
134 |
135 class pcpo = cpo + |
135 class pcpo = cpo + |
136 assumes least: "\<exists>x. \<forall>y. x \<sqsubseteq> y" |
136 assumes least: "\<exists>x. \<forall>y. x \<sqsubseteq> y" |
137 begin |
137 begin |
138 |
138 |
139 definition bottom :: "'a" ("\<bottom>") |
139 definition bottom :: "'a" (\<open>\<bottom>\<close>) |
140 where "bottom = (THE x. \<forall>y. x \<sqsubseteq> y)" |
140 where "bottom = (THE x. \<forall>y. x \<sqsubseteq> y)" |
141 |
141 |
142 lemma minimal [iff]: "\<bottom> \<sqsubseteq> x" |
142 lemma minimal [iff]: "\<bottom> \<sqsubseteq> x" |
143 unfolding bottom_def |
143 unfolding bottom_def |
144 apply (rule the1I2) |
144 apply (rule the1I2) |