changeset 12114 | a8e860c86252 |
parent 11441 | 54b236801671 |
child 12399 | 2ba27248af7f |
--- a/src/HOL/Lattice/CompleteLattice.thy Fri Nov 09 00:06:15 2001 +0100 +++ b/src/HOL/Lattice/CompleteLattice.thy Fri Nov 09 00:09:47 2001 +0100 @@ -34,7 +34,7 @@ consts Meet :: "'a::complete_lattice set \<Rightarrow> 'a" Join :: "'a::complete_lattice set \<Rightarrow> 'a" -syntax (symbols) +syntax (xsymbols) Meet :: "'a::complete_lattice set \<Rightarrow> 'a" ("\<Sqinter>_" [90] 90) Join :: "'a::complete_lattice set \<Rightarrow> 'a" ("\<Squnion>_" [90] 90) defs