changeset 26806 | 40b411ec05aa |
parent 26454 | 57923fdab83b |
child 26927 | 8684b5240f11 |
--- a/src/HOLCF/CompactBasis.thy Wed May 07 10:56:58 2008 +0200 +++ b/src/HOLCF/CompactBasis.thy Wed May 07 10:57:19 2008 +0200 @@ -227,7 +227,7 @@ lemma lessI: "(\<And>a. principal a \<sqsubseteq> x \<Longrightarrow> principal a \<sqsubseteq> u) \<Longrightarrow> x \<sqsubseteq> u" unfolding principal_less_iff -by (simp add: less_def subset_def) +by (simp add: less_def subset_eq) lemma lub_principal_approxes: "principal ` approxes x <<| x" apply (rule is_lubI)