changeset 12114 | a8e860c86252 |
parent 12023 | d982f98e0f0d |
child 12257 | e3f7d6fb55d7 |
--- a/src/HOL/Set.thy Fri Nov 09 00:06:15 2001 +0100 +++ b/src/HOL/Set.thy Fri Nov 09 00:09:47 2001 +0100 @@ -91,7 +91,7 @@ "_setless" :: "'a set => 'a set => bool" ("op <") "_setless" :: "'a set => 'a set => bool" ("(_/ < _)" [50, 51] 50) -syntax (symbols) +syntax (xsymbols) "_setle" :: "'a set => 'a set => bool" ("op \<subseteq>") "_setle" :: "'a set => 'a set => bool" ("(_/ \<subseteq> _)" [50, 51] 50) "_setless" :: "'a set => 'a set => bool" ("op \<subset>")