changeset 41082 | 9ff94e7cc3b3 |
parent 41080 | 294956ff285b |
child 43753 | fe5e846c0839 |
--- a/src/HOL/Lattices.thy Wed Dec 08 14:52:23 2010 +0100 +++ b/src/HOL/Lattices.thy Wed Dec 08 15:05:46 2010 +0100 @@ -48,8 +48,9 @@ notation less_eq (infix "\<sqsubseteq>" 50) and less (infix "\<sqsubset>" 50) and - top ("\<top>") and - bot ("\<bottom>") + bot ("\<bottom>") and + top ("\<top>") + class semilattice_inf = order + fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)