changeset 21210 | c17fd2df4e9e |
parent 20523 | 36a59e5d0039 |
child 21404 | eb85850d3eb7 |
--- a/src/HOL/Lattice/Lattice.thy Tue Nov 07 11:47:56 2006 +0100 +++ b/src/HOL/Lattice/Lattice.thy Tue Nov 07 11:47:57 2006 +0100 @@ -30,7 +30,7 @@ join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "||" 65) "x || y = (THE sup. is_sup x y sup)" -const_syntax (xsymbols) +notation (xsymbols) meet (infixl "\<sqinter>" 70) join (infixl "\<squnion>" 65)