equal
deleted
inserted
replaced
781 lemma top_eq: "\<lbrakk> t \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> x \<sqsubseteq> t \<rbrakk> \<Longrightarrow> t = \<top>" |
781 lemma top_eq: "\<lbrakk> t \<in> carrier L; \<And> x. x \<in> carrier L \<Longrightarrow> x \<sqsubseteq> t \<rbrakk> \<Longrightarrow> t = \<top>" |
782 by (metis le_antisym top_closed top_higher) |
782 by (metis le_antisym top_closed top_higher) |
783 |
783 |
784 end |
784 end |
785 |
785 |
|
786 hide_const (open) Lattice.inf |
|
787 hide_const (open) Lattice.sup |
|
788 |
786 end |
789 end |