changeset 21210 | c17fd2df4e9e |
parent 19736 | d8d0f8f51d69 |
child 21404 | eb85850d3eb7 |
--- a/src/HOL/Lattice/CompleteLattice.thy Tue Nov 07 11:47:56 2006 +0100 +++ b/src/HOL/Lattice/CompleteLattice.thy Tue Nov 07 11:47:57 2006 +0100 @@ -37,7 +37,7 @@ Join :: "'a::complete_lattice set \<Rightarrow> 'a" "Join A = (THE sup. is_Sup A sup)" -const_syntax (xsymbols) +notation (xsymbols) Meet ("\<Sqinter>_" [90] 90) Join ("\<Squnion>_" [90] 90)