some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
authorwenzelm
Tue, 20 Nov 2012 22:53:59 +0100
changeset 50137 0226d408058b
parent 50136 a96bd08258a2
child 50138 ca989d793b34
some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
etc/symbols
--- a/etc/symbols	Tue Nov 20 22:52:04 2012 +0100
+++ b/etc/symbols	Tue Nov 20 22:53:59 2012 +0100
@@ -10,305 +10,305 @@
 \<seven>                code: 0x01d7f3
 \<eight>                code: 0x01d7f4
 \<nine>                 code: 0x01d7f5
-\<A>                    code: 0x01d49c
-\<B>                    code: 0x00212c
-\<C>                    code: 0x01d49e
-\<D>                    code: 0x01d49f
-\<E>                    code: 0x002130
-\<F>                    code: 0x002131
-\<G>                    code: 0x01d4a2
-\<H>                    code: 0x00210b
-\<I>                    code: 0x002110
-\<J>                    code: 0x01d4a5
-\<K>                    code: 0x01d4a6
-\<L>                    code: 0x002112
-\<M>                    code: 0x002133
-\<N>                    code: 0x01d4a9
-\<O>                    code: 0x01d4aa
-\<P>                    code: 0x01d4ab
-\<Q>                    code: 0x01d4ac
-\<R>                    code: 0x00211b
-\<S>                    code: 0x01d4ae
-\<T>                    code: 0x01d4af
-\<U>                    code: 0x01d4b0
-\<V>                    code: 0x01d4b1
-\<W>                    code: 0x01d4b2
-\<X>                    code: 0x01d4b3
-\<Y>                    code: 0x01d4b4
-\<Z>                    code: 0x01d4b5
-\<a>                    code: 0x01d5ba
-\<b>                    code: 0x01d5bb
-\<c>                    code: 0x01d5bc
-\<d>                    code: 0x01d5bd
-\<e>                    code: 0x01d5be
-\<f>                    code: 0x01d5bf
-\<g>                    code: 0x01d5c0
-\<h>                    code: 0x01d5c1
-\<i>                    code: 0x01d5c2
-\<j>                    code: 0x01d5c3
-\<k>                    code: 0x01d5c4
-\<l>                    code: 0x01d5c5
-\<m>                    code: 0x01d5c6
-\<n>                    code: 0x01d5c7
-\<o>                    code: 0x01d5c8
-\<p>                    code: 0x01d5c9
-\<q>                    code: 0x01d5ca
-\<r>                    code: 0x01d5cb
-\<s>                    code: 0x01d5cc
-\<t>                    code: 0x01d5cd
-\<u>                    code: 0x01d5ce
-\<v>                    code: 0x01d5cf
-\<w>                    code: 0x01d5d0
-\<x>                    code: 0x01d5d1
-\<y>                    code: 0x01d5d2
-\<z>                    code: 0x01d5d3
-\<AA>                   code: 0x01d504
-\<BB>                   code: 0x01d505
-\<CC>                   code: 0x00212d
-\<DD>                   code: 0x01d507
-\<EE>                   code: 0x01d508
-\<FF>                   code: 0x01d509
-\<GG>                   code: 0x01d50a
-\<HH>                   code: 0x00210c
-\<II>                   code: 0x002111
-\<JJ>                   code: 0x01d50d
-\<KK>                   code: 0x01d50e
-\<LL>                   code: 0x01d50f
-\<MM>                   code: 0x01d510
-\<NN>                   code: 0x01d511
-\<OO>                   code: 0x01d512
-\<PP>                   code: 0x01d513
-\<QQ>                   code: 0x01d514
-\<RR>                   code: 0x00211c
-\<SS>                   code: 0x01d516
-\<TT>                   code: 0x01d517
-\<UU>                   code: 0x01d518
-\<VV>                   code: 0x01d519
-\<WW>                   code: 0x01d51a
-\<XX>                   code: 0x01d51b
-\<YY>                   code: 0x01d51c
-\<ZZ>                   code: 0x002128
-\<aa>                   code: 0x01d51e
-\<bb>                   code: 0x01d51f
-\<cc>                   code: 0x01d520
-\<dd>                   code: 0x01d521
-\<ee>                   code: 0x01d522
-\<ff>                   code: 0x01d523
-\<gg>                   code: 0x01d524
-\<hh>                   code: 0x01d525
-\<ii>                   code: 0x01d526
-\<jj>                   code: 0x01d527
-\<kk>                   code: 0x01d528
-\<ll>                   code: 0x01d529
-\<mm>                   code: 0x01d52a
-\<nn>                   code: 0x01d52b
-\<oo>                   code: 0x01d52c
-\<pp>                   code: 0x01d52d
-\<qq>                   code: 0x01d52e
-\<rr>                   code: 0x01d52f
-\<ss>                   code: 0x01d530
-\<tt>                   code: 0x01d531
-\<uu>                   code: 0x01d532
-\<vv>                   code: 0x01d533
-\<ww>                   code: 0x01d534
-\<xx>                   code: 0x01d535
-\<yy>                   code: 0x01d536
-\<zz>                   code: 0x01d537
-\<alpha>                code: 0x0003b1
-\<beta>                 code: 0x0003b2
-\<gamma>                code: 0x0003b3
-\<delta>                code: 0x0003b4
-\<epsilon>              code: 0x0003b5
-\<zeta>                 code: 0x0003b6
-\<eta>                  code: 0x0003b7
-\<theta>                code: 0x0003b8
-\<iota>                 code: 0x0003b9
-\<kappa>                code: 0x0003ba
-\<lambda>               code: 0x0003bb  abbrev: %
-\<mu>                   code: 0x0003bc
-\<nu>                   code: 0x0003bd
-\<xi>                   code: 0x0003be
-\<pi>                   code: 0x0003c0
-\<rho>                  code: 0x0003c1
-\<sigma>                code: 0x0003c3
-\<tau>                  code: 0x0003c4
-\<upsilon>              code: 0x0003c5
-\<phi>                  code: 0x0003c6
-\<chi>                  code: 0x0003c7
-\<psi>                  code: 0x0003c8
-\<omega>                code: 0x0003c9
-\<Gamma>                code: 0x000393
-\<Delta>                code: 0x000394
-\<Theta>                code: 0x000398
-\<Lambda>               code: 0x00039b
-\<Xi>                   code: 0x00039e
-\<Pi>                   code: 0x0003a0
-\<Sigma>                code: 0x0003a3
-\<Upsilon>              code: 0x0003a5
-\<Phi>                  code: 0x0003a6
-\<Psi>                  code: 0x0003a8
-\<Omega>                code: 0x0003a9
-\<bool>                 code: 0x01d539
-\<complex>              code: 0x002102
-\<nat>                  code: 0x002115
-\<rat>                  code: 0x00211a
-\<real>                 code: 0x00211d
-\<int>                  code: 0x002124
-\<leftarrow>            code: 0x002190
-\<longleftarrow>        code: 0x0027f5
-\<rightarrow>           code: 0x002192  abbrev: ->
-\<longrightarrow>       code: 0x0027f6  abbrev: -->
-\<Leftarrow>            code: 0x0021d0
-\<Longleftarrow>        code: 0x0027f8
-\<Rightarrow>           code: 0x0021d2  abbrev: =>
-\<Longrightarrow>       code: 0x0027f9  abbrev: ==>
-\<leftrightarrow>       code: 0x002194
-\<longleftrightarrow>   code: 0x0027f7  abbrev: <->
-\<Leftrightarrow>       code: 0x0021d4
-\<Longleftrightarrow>   code: 0x0027fa  abbrev: <=>
-\<mapsto>               code: 0x0021a6  abbrev: |->
-\<longmapsto>           code: 0x0027fc  abbrev: |-->
-\<midarrow>             code: 0x002500
-\<Midarrow>             code: 0x002550
-\<hookleftarrow>        code: 0x0021a9
-\<hookrightarrow>       code: 0x0021aa
-\<leftharpoondown>      code: 0x0021bd
-\<rightharpoondown>     code: 0x0021c1
-\<leftharpoonup>        code: 0x0021bc
-\<rightharpoonup>       code: 0x0021c0
-\<rightleftharpoons>    code: 0x0021cc
-\<leadsto>              code: 0x00219d  abbrev: ~>
-\<downharpoonleft>      code: 0x0021c3
-\<downharpoonright>     code: 0x0021c2
-\<upharpoonleft>        code: 0x0021bf
-#\<upharpoonright>       code: 0x0021be
-\<restriction>          code: 0x0021be
-\<Colon>                code: 0x002237
-\<up>                   code: 0x002191
-\<Up>                   code: 0x0021d1
-\<down>                 code: 0x002193
-\<Down>                 code: 0x0021d3
-\<updown>               code: 0x002195
-\<Updown>               code: 0x0021d5
-\<langle>               code: 0x0027e8  abbrev: <.
-\<rangle>               code: 0x0027e9  abbrev: .>
-\<lceil>                code: 0x002308
-\<rceil>                code: 0x002309
-\<lfloor>               code: 0x00230a
-\<rfloor>               code: 0x00230b
-\<lparr>                code: 0x002987  abbrev: (|
-\<rparr>                code: 0x002988  abbrev: |)
-\<lbrakk>               code: 0x0027e6  abbrev: [|
-\<rbrakk>               code: 0x0027e7  abbrev: |]
-\<lbrace>               code: 0x002983  abbrev: {.
-\<rbrace>               code: 0x002984  abbrev: .}
-\<guillemotleft>        code: 0x0000ab  abbrev: <<
-\<guillemotright>       code: 0x0000bb  abbrev: >>
-\<bottom>               code: 0x0022a5
-\<top>                  code: 0x0022a4
-\<and>                  code: 0x002227  abbrev: /\
-\<And>                  code: 0x0022c0  abbrev: !!
-\<or>                   code: 0x002228  abbrev: \/
-\<Or>                   code: 0x0022c1  abbrev: ??
+\<A>                    code: 0x01d49c  group: letter
+\<B>                    code: 0x00212c  group: letter
+\<C>                    code: 0x01d49e  group: letter
+\<D>                    code: 0x01d49f  group: letter
+\<E>                    code: 0x002130  group: letter
+\<F>                    code: 0x002131  group: letter
+\<G>                    code: 0x01d4a2  group: letter
+\<H>                    code: 0x00210b  group: letter
+\<I>                    code: 0x002110  group: letter
+\<J>                    code: 0x01d4a5  group: letter
+\<K>                    code: 0x01d4a6  group: letter
+\<L>                    code: 0x002112  group: letter
+\<M>                    code: 0x002133  group: letter
+\<N>                    code: 0x01d4a9  group: letter
+\<O>                    code: 0x01d4aa  group: letter
+\<P>                    code: 0x01d4ab  group: letter
+\<Q>                    code: 0x01d4ac  group: letter
+\<R>                    code: 0x00211b  group: letter
+\<S>                    code: 0x01d4ae  group: letter
+\<T>                    code: 0x01d4af  group: letter
+\<U>                    code: 0x01d4b0  group: letter
+\<V>                    code: 0x01d4b1  group: letter
+\<W>                    code: 0x01d4b2  group: letter
+\<X>                    code: 0x01d4b3  group: letter
+\<Y>                    code: 0x01d4b4  group: letter
+\<Z>                    code: 0x01d4b5  group: letter
+\<a>                    code: 0x01d5ba  group: letter
+\<b>                    code: 0x01d5bb  group: letter
+\<c>                    code: 0x01d5bc  group: letter
+\<d>                    code: 0x01d5bd  group: letter
+\<e>                    code: 0x01d5be  group: letter
+\<f>                    code: 0x01d5bf  group: letter
+\<g>                    code: 0x01d5c0  group: letter
+\<h>                    code: 0x01d5c1  group: letter
+\<i>                    code: 0x01d5c2  group: letter
+\<j>                    code: 0x01d5c3  group: letter
+\<k>                    code: 0x01d5c4  group: letter
+\<l>                    code: 0x01d5c5  group: letter
+\<m>                    code: 0x01d5c6  group: letter
+\<n>                    code: 0x01d5c7  group: letter
+\<o>                    code: 0x01d5c8  group: letter
+\<p>                    code: 0x01d5c9  group: letter
+\<q>                    code: 0x01d5ca  group: letter
+\<r>                    code: 0x01d5cb  group: letter
+\<s>                    code: 0x01d5cc  group: letter
+\<t>                    code: 0x01d5cd  group: letter
+\<u>                    code: 0x01d5ce  group: letter
+\<v>                    code: 0x01d5cf  group: letter
+\<w>                    code: 0x01d5d0  group: letter
+\<x>                    code: 0x01d5d1  group: letter
+\<y>                    code: 0x01d5d2  group: letter
+\<z>                    code: 0x01d5d3  group: letter
+\<AA>                   code: 0x01d504  group: letter
+\<BB>                   code: 0x01d505  group: letter
+\<CC>                   code: 0x00212d  group: letter
+\<DD>                   code: 0x01d507  group: letter
+\<EE>                   code: 0x01d508  group: letter
+\<FF>                   code: 0x01d509  group: letter
+\<GG>                   code: 0x01d50a  group: letter
+\<HH>                   code: 0x00210c  group: letter
+\<II>                   code: 0x002111  group: letter
+\<JJ>                   code: 0x01d50d  group: letter
+\<KK>                   code: 0x01d50e  group: letter
+\<LL>                   code: 0x01d50f  group: letter
+\<MM>                   code: 0x01d510  group: letter
+\<NN>                   code: 0x01d511  group: letter
+\<OO>                   code: 0x01d512  group: letter
+\<PP>                   code: 0x01d513  group: letter
+\<QQ>                   code: 0x01d514  group: letter
+\<RR>                   code: 0x00211c  group: letter
+\<SS>                   code: 0x01d516  group: letter
+\<TT>                   code: 0x01d517  group: letter
+\<UU>                   code: 0x01d518  group: letter
+\<VV>                   code: 0x01d519  group: letter
+\<WW>                   code: 0x01d51a  group: letter
+\<XX>                   code: 0x01d51b  group: letter
+\<YY>                   code: 0x01d51c  group: letter
+\<ZZ>                   code: 0x002128  group: letter
+\<aa>                   code: 0x01d51e  group: letter
+\<bb>                   code: 0x01d51f  group: letter
+\<cc>                   code: 0x01d520  group: letter
+\<dd>                   code: 0x01d521  group: letter
+\<ee>                   code: 0x01d522  group: letter
+\<ff>                   code: 0x01d523  group: letter
+\<gg>                   code: 0x01d524  group: letter
+\<hh>                   code: 0x01d525  group: letter
+\<ii>                   code: 0x01d526  group: letter
+\<jj>                   code: 0x01d527  group: letter
+\<kk>                   code: 0x01d528  group: letter
+\<ll>                   code: 0x01d529  group: letter
+\<mm>                   code: 0x01d52a  group: letter
+\<nn>                   code: 0x01d52b  group: letter
+\<oo>                   code: 0x01d52c  group: letter
+\<pp>                   code: 0x01d52d  group: letter
+\<qq>                   code: 0x01d52e  group: letter
+\<rr>                   code: 0x01d52f  group: letter
+\<ss>                   code: 0x01d530  group: letter
+\<tt>                   code: 0x01d531  group: letter
+\<uu>                   code: 0x01d532  group: letter
+\<vv>                   code: 0x01d533  group: letter
+\<ww>                   code: 0x01d534  group: letter
+\<xx>                   code: 0x01d535  group: letter
+\<yy>                   code: 0x01d536  group: letter
+\<zz>                   code: 0x01d537  group: letter
+\<alpha>                code: 0x0003b1  group: greek
+\<beta>                 code: 0x0003b2  group: greek
+\<gamma>                code: 0x0003b3  group: greek
+\<delta>                code: 0x0003b4  group: greek
+\<epsilon>              code: 0x0003b5  group: greek
+\<zeta>                 code: 0x0003b6  group: greek
+\<eta>                  code: 0x0003b7  group: greek
+\<theta>                code: 0x0003b8  group: greek
+\<iota>                 code: 0x0003b9  group: greek
+\<kappa>                code: 0x0003ba  group: greek
+\<lambda>               code: 0x0003bb  group: greek  abbrev: %
+\<mu>                   code: 0x0003bc  group: greek
+\<nu>                   code: 0x0003bd  group: greek
+\<xi>                   code: 0x0003be  group: greek
+\<pi>                   code: 0x0003c0  group: greek
+\<rho>                  code: 0x0003c1  group: greek
+\<sigma>                code: 0x0003c3  group: greek
+\<tau>                  code: 0x0003c4  group: greek
+\<upsilon>              code: 0x0003c5  group: greek
+\<phi>                  code: 0x0003c6  group: greek
+\<chi>                  code: 0x0003c7  group: greek
+\<psi>                  code: 0x0003c8  group: greek
+\<omega>                code: 0x0003c9  group: greek
+\<Gamma>                code: 0x000393  group: greek
+\<Delta>                code: 0x000394  group: greek
+\<Theta>                code: 0x000398  group: greek
+\<Lambda>               code: 0x00039b  group: greek
+\<Xi>                   code: 0x00039e  group: greek
+\<Pi>                   code: 0x0003a0  group: greek
+\<Sigma>                code: 0x0003a3  group: greek
+\<Upsilon>              code: 0x0003a5  group: greek
+\<Phi>                  code: 0x0003a6  group: greek
+\<Psi>                  code: 0x0003a8  group: greek
+\<Omega>                code: 0x0003a9  group: greek
+\<bool>                 code: 0x01d539  group: letter
+\<complex>              code: 0x002102  group: letter
+\<nat>                  code: 0x002115  group: letter
+\<rat>                  code: 0x00211a  group: letter
+\<real>                 code: 0x00211d  group: letter
+\<int>                  code: 0x002124  group: letter
+\<leftarrow>            code: 0x002190  group: arrow
+\<longleftarrow>        code: 0x0027f5  group: arrow
+\<rightarrow>           code: 0x002192  group: arrow  abbrev: ->
+\<longrightarrow>       code: 0x0027f6  group: arrow  abbrev: -->
+\<Leftarrow>            code: 0x0021d0  group: arrow
+\<Longleftarrow>        code: 0x0027f8  group: arrow
+\<Rightarrow>           code: 0x0021d2  group: arrow  abbrev: =>
+\<Longrightarrow>       code: 0x0027f9  group: arrow  abbrev: ==>
+\<leftrightarrow>       code: 0x002194  group: arrow
+\<longleftrightarrow>   code: 0x0027f7  group: arrow  abbrev: <->
+\<Leftrightarrow>       code: 0x0021d4  group: arrow
+\<Longleftrightarrow>   code: 0x0027fa  group: arrow  abbrev: <=>
+\<mapsto>               code: 0x0021a6  group: arrow  abbrev: |->
+\<longmapsto>           code: 0x0027fc  group: arrow  abbrev: |-->
+\<midarrow>             code: 0x002500  group: arrow
+\<Midarrow>             code: 0x002550  group: arrow
+\<hookleftarrow>        code: 0x0021a9  group: arrow
+\<hookrightarrow>       code: 0x0021aa  group: arrow
+\<leftharpoondown>      code: 0x0021bd  group: arrow
+\<rightharpoondown>     code: 0x0021c1  group: arrow
+\<leftharpoonup>        code: 0x0021bc  group: arrow
+\<rightharpoonup>       code: 0x0021c0  group: arrow
+\<rightleftharpoons>    code: 0x0021cc  group: arrow
+\<leadsto>              code: 0x00219d  group: arrow  abbrev: ~>
+\<downharpoonleft>      code: 0x0021c3  group: arrow
+\<downharpoonright>     code: 0x0021c2  group: arrow
+\<upharpoonleft>        code: 0x0021bf  group: arrow
+#\<upharpoonright>       code: 0x0021be  group: arrow
+\<restriction>          code: 0x0021be  group: punctuation
+\<Colon>                code: 0x002237  group: punctuation
+\<up>                   code: 0x002191  group: arrow
+\<Up>                   code: 0x0021d1  group: arrow
+\<down>                 code: 0x002193  group: arrow
+\<Down>                 code: 0x0021d3  group: arrow
+\<updown>               code: 0x002195  group: arrow
+\<Updown>               code: 0x0021d5  group: arrow
+\<langle>               code: 0x0027e8  group: punctuation  abbrev: <.
+\<rangle>               code: 0x0027e9  group: punctuation  abbrev: .>
+\<lceil>                code: 0x002308  group: punctuation
+\<rceil>                code: 0x002309  group: punctuation
+\<lfloor>               code: 0x00230a  group: punctuation
+\<rfloor>               code: 0x00230b  group: punctuation
+\<lparr>                code: 0x002987  group: punctuation  abbrev: (|
+\<rparr>                code: 0x002988  group: punctuation  abbrev: |)
+\<lbrakk>               code: 0x0027e6  group: punctuation  abbrev: [|
+\<rbrakk>               code: 0x0027e7  group: punctuation  abbrev: |]
+\<lbrace>               code: 0x002983  group: punctuation  abbrev: {.
+\<rbrace>               code: 0x002984  group: punctuation  abbrev: .}
+\<guillemotleft>        code: 0x0000ab  group: punctuation  abbrev: <<
+\<guillemotright>       code: 0x0000bb  group: punctuation  abbrev: >>
+\<bottom>               code: 0x0022a5  group: arrow
+\<top>                  code: 0x0022a4  group: arrow
+\<and>                  code: 0x002227  group: operator  abbrev: /\
+\<And>                  code: 0x0022c0  group: operator  abbrev: !!
+\<or>                   code: 0x002228  group: operator  abbrev: \/
+\<Or>                   code: 0x0022c1  group: operator  abbrev: ??
 \<forall>               code: 0x002200  abbrev: !
 \<exists>               code: 0x002203  abbrev: ?
 \<nexists>              code: 0x002204  abbrev: ~?
 \<not>                  code: 0x0000ac  abbrev: ~
 \<box>                  code: 0x0025a1
 \<diamond>              code: 0x0025c7
-\<turnstile>            code: 0x0022a2  abbrev: |-
-\<Turnstile>            code: 0x0022a8  abbrev: |=
-\<tturnstile>           code: 0x0022a9  abbrev: ||-
-\<TTurnstile>           code: 0x0022ab  abbrev: ||=
-\<stileturn>            code: 0x0022a3  abbrev: -|
-\<surd>                 code: 0x00221a
-\<le>                   code: 0x002264  abbrev: <=
-\<ge>                   code: 0x002265  abbrev: >=
-\<lless>                code: 0x00226a
-\<ggreater>             code: 0x00226b
-\<lesssim>              code: 0x002272
-\<greatersim>           code: 0x002273
-\<lessapprox>           code: 0x002a85
-\<greaterapprox>        code: 0x002a86
-\<in>                   code: 0x002208  abbrev: :
-\<notin>                code: 0x002209  abbrev: ~:
-\<subset>               code: 0x002282
-\<supset>               code: 0x002283
-\<subseteq>             code: 0x002286  abbrev: (=
-\<supseteq>             code: 0x002287  abbrev: =)
-\<sqsubset>             code: 0x00228f
-\<sqsupset>             code: 0x002290
-\<sqsubseteq>           code: 0x002291  abbrev: [=
-\<sqsupseteq>           code: 0x002292  abbrev: =]
-\<inter>                code: 0x002229  abbrev: Int
-\<Inter>                code: 0x0022c2  abbrev: Inter
-\<union>                code: 0x00222a  abbrev: Un
-\<Union>                code: 0x0022c3  abbrev: Union
-\<squnion>              code: 0x002294
-\<Squnion>              code: 0x002a06
-\<sqinter>              code: 0x002293
-\<Sqinter>              code: 0x002a05
-\<setminus>             code: 0x002216
-\<propto>               code: 0x00221d
-\<uplus>                code: 0x00228e
-\<Uplus>                code: 0x002a04
-\<noteq>                code: 0x002260  abbrev: ~=
-\<sim>                  code: 0x00223c
-\<doteq>                code: 0x002250
-\<simeq>                code: 0x002243
-\<approx>               code: 0x002248
-\<asymp>                code: 0x00224d
-\<cong>                 code: 0x002245
-\<smile>                code: 0x002323
-\<equiv>                code: 0x002261  abbrev: ==
-\<frown>                code: 0x002322
+\<turnstile>            code: 0x0022a2  group: relation  abbrev: |-
+\<Turnstile>            code: 0x0022a8  group: relation  abbrev: |=
+\<tturnstile>           code: 0x0022a9  group: relation  abbrev: ||-
+\<TTurnstile>           code: 0x0022ab  group: relation  abbrev: ||=
+\<stileturn>            code: 0x0022a3  group: relation  abbrev: -|
+\<surd>                 code: 0x00221a  group: relation
+\<le>                   code: 0x002264  group: relation  abbrev: <=
+\<ge>                   code: 0x002265  group: relation  abbrev: >=
+\<lless>                code: 0x00226a  group: relation
+\<ggreater>             code: 0x00226b  group: relation
+\<lesssim>              code: 0x002272  group: relation
+\<greatersim>           code: 0x002273  group: relation
+\<lessapprox>           code: 0x002a85  group: relation
+\<greaterapprox>        code: 0x002a86  group: relation
+\<in>                   code: 0x002208  group: relation  abbrev: :
+\<notin>                code: 0x002209  group: relation  abbrev: ~:
+\<subset>               code: 0x002282  group: relation
+\<supset>               code: 0x002283  group: relation
+\<subseteq>             code: 0x002286  group: relation  abbrev: (=
+\<supseteq>             code: 0x002287  group: relation  abbrev: =)
+\<sqsubset>             code: 0x00228f  group: relation
+\<sqsupset>             code: 0x002290  group: relation
+\<sqsubseteq>           code: 0x002291  group: relation  abbrev: [=
+\<sqsupseteq>           code: 0x002292  group: relation  abbrev: =]
+\<inter>                code: 0x002229  group: operator  abbrev: Int
+\<Inter>                code: 0x0022c2  group: operator  abbrev: Inter
+\<union>                code: 0x00222a  group: operator  abbrev: Un
+\<Union>                code: 0x0022c3  group: operator  abbrev: Union
+\<squnion>              code: 0x002294  group: operator
+\<Squnion>              code: 0x002a06  group: operator
+\<sqinter>              code: 0x002293  group: operator
+\<Sqinter>              code: 0x002a05  group: operator
+\<setminus>             code: 0x002216  group: operator
+\<propto>               code: 0x00221d  group: operator
+\<uplus>                code: 0x00228e  group: operator
+\<Uplus>                code: 0x002a04  group: operator
+\<noteq>                code: 0x002260  group: relation  abbrev: ~=
+\<sim>                  code: 0x00223c  group: relation
+\<doteq>                code: 0x002250  group: relation
+\<simeq>                code: 0x002243  group: relation
+\<approx>               code: 0x002248  group: relation
+\<asymp>                code: 0x00224d  group: relation
+\<cong>                 code: 0x002245  group: relation
+\<smile>                code: 0x002323  group: relation
+\<equiv>                code: 0x002261  group: relation  abbrev: ==
+\<frown>                code: 0x002322  group: relation
 \<Join>                 code: 0x0022c8
 \<bowtie>               code: 0x002a1d
-\<prec>                 code: 0x00227a
-\<succ>                 code: 0x00227b
-\<preceq>               code: 0x00227c
-\<succeq>               code: 0x00227d
-\<parallel>             code: 0x002225  abbrev: ||
-\<bar>                  code: 0x0000a6
-\<plusminus>            code: 0x0000b1
-\<minusplus>            code: 0x002213
-\<times>                code: 0x0000d7
-\<div>                  code: 0x0000f7
-\<cdot>                 code: 0x0022c5
-\<star>                 code: 0x0022c6
-\<bullet>               code: 0x002219
-\<circ>                 code: 0x002218
+\<prec>                 code: 0x00227a  group: relation
+\<succ>                 code: 0x00227b  group: relation
+\<preceq>               code: 0x00227c  group: relation
+\<succeq>               code: 0x00227d  group: relation
+\<parallel>             code: 0x002225  group: punctuation  abbrev: ||
+\<bar>                  code: 0x0000a6  group: punctuation
+\<plusminus>            code: 0x0000b1  group: operator
+\<minusplus>            code: 0x002213  group: operator
+\<times>                code: 0x0000d7  group: operator
+\<div>                  code: 0x0000f7  group: operator
+\<cdot>                 code: 0x0022c5  group: operator
+\<star>                 code: 0x0022c6  group: operator
+\<bullet>               code: 0x002219  group: operator
+\<circ>                 code: 0x002218  group: operator
 \<dagger>               code: 0x002020
 \<ddagger>              code: 0x002021
-\<lhd>                  code: 0x0022b2
-\<rhd>                  code: 0x0022b3
-\<unlhd>                code: 0x0022b4
-\<unrhd>                code: 0x0022b5
-\<triangleleft>         code: 0x0025c3
-\<triangleright>        code: 0x0025b9
-\<triangle>             code: 0x0025b3
-\<triangleq>            code: 0x00225c
-\<oplus>                code: 0x002295  abbrev: +o
-\<Oplus>                code: 0x002a01  abbrev: +O
-\<otimes>               code: 0x002297  abbrev: *o
-\<Otimes>               code: 0x002a02  abbrev: *O
-\<odot>                 code: 0x002299  abbrev: .o
-\<Odot>                 code: 0x002a00  abbrev: .O
-\<ominus>               code: 0x002296  abbrev: -o
-\<oslash>               code: 0x002298  abbrev: /o
+\<lhd>                  code: 0x0022b2  group: relation
+\<rhd>                  code: 0x0022b3  group: relation
+\<unlhd>                code: 0x0022b4  group: relation
+\<unrhd>                code: 0x0022b5  group: relation
+\<triangleleft>         code: 0x0025c3  group: relation
+\<triangleright>        code: 0x0025b9  group: relation
+\<triangle>             code: 0x0025b3  group: relation
+\<triangleq>            code: 0x00225c  group: relation
+\<oplus>                code: 0x002295  group: operator  abbrev: +o
+\<Oplus>                code: 0x002a01  group: operator  abbrev: +O
+\<otimes>               code: 0x002297  group: operator  abbrev: *o
+\<Otimes>               code: 0x002a02  group: operator  abbrev: *O
+\<odot>                 code: 0x002299  group: operator  abbrev: .o
+\<Odot>                 code: 0x002a00  group: operator  abbrev: .O
+\<ominus>               code: 0x002296  group: operator  abbrev: -o
+\<oslash>               code: 0x002298  group: operator  abbrev: /o
 \<dots>                 code: 0x002026  abbrev: ...
 \<cdots>                code: 0x0022ef
-\<Sum>                  code: 0x002211  abbrev: SUM
-\<Prod>                 code: 0x00220f  abbrev: PROD
-\<Coprod>               code: 0x002210
+\<Sum>                  code: 0x002211  group: operator  abbrev: SUM
+\<Prod>                 code: 0x00220f  group: operator  abbrev: PROD
+\<Coprod>               code: 0x002210  group: operator
 \<infinity>             code: 0x00221e
-\<integral>             code: 0x00222b
-\<ointegral>            code: 0x00222e
+\<integral>             code: 0x00222b  group: operator
+\<ointegral>            code: 0x00222e  group: operator
 \<clubsuit>             code: 0x002663
 \<diamondsuit>          code: 0x002662
 \<heartsuit>            code: 0x002661
 \<spadesuit>            code: 0x002660
-\<aleph>                code: 0x002135
+\<aleph>                code: 0x002135  group: letter
 \<emptyset>             code: 0x002205
 \<nabla>                code: 0x002207
 \<partial>              code: 0x002202
@@ -318,8 +318,8 @@
 \<angle>                code: 0x002220
 \<copyright>            code: 0x0000a9
 \<registered>           code: 0x0000ae
-\<hyphen>               code: 0x0000ad
-\<inverse>              code: 0x0000af
+\<hyphen>               code: 0x0000ad  group: punctuation
+\<inverse>              code: 0x0000af  group: punctuation
 \<onesuperior>          code: 0x0000b9
 \<onequarter>           code: 0x0000bc
 \<twosuperior>          code: 0x0000b2
@@ -338,11 +338,11 @@
 \<cent>                 code: 0x0000a2
 \<currency>             code: 0x0000a4
 \<degree>               code: 0x0000b0
-\<amalg>                code: 0x002a3f
-\<mho>                  code: 0x002127
+\<amalg>                code: 0x002a3f  group: operator
+\<mho>                  code: 0x002127  group: operator
 \<lozenge>              code: 0x0025ca
-\<wp>                   code: 0x002118
-\<wrong>                code: 0x002240
+\<wp>                   code: 0x002118  group: letter
+\<wrong>                code: 0x002240  group: relation
 \<struct>               code: 0x0022c4
 \<acute>                code: 0x0000b4
 \<index>                code: 0x000131
@@ -350,13 +350,13 @@
 \<cedilla>              code: 0x0000b8
 \<hungarumlaut>         code: 0x0002dd
 \<some>                 code: 0x0003f5
-\<^sub>                 code: 0x0021e9  abbrev: =_
-\<^sup>                 code: 0x0021e7  abbrev: =^
-\<^isub>                code: 0x0021e3  abbrev: -_
-\<^isup>                code: 0x0021e1  abbrev: -^
-\<^bsub>                code: 0x0021d8  abbrev: =_(
-\<^esub>                code: 0x0021d9  abbrev: =_)
-\<^bsup>                code: 0x0021d7  abbrev: =^(
-\<^esup>                code: 0x0021d6  abbrev: =^)
-\<^bold>                code: 0x002759  abbrev: -.
+\<^sub>                 code: 0x0021e9  group: control  abbrev: =_
+\<^sup>                 code: 0x0021e7  group: control  abbrev: =^
+\<^isub>                code: 0x0021e3  group: control  abbrev: -_
+\<^isup>                code: 0x0021e1  group: control  abbrev: -^
+\<^bsub>                code: 0x0021d8  group: control  abbrev: =_(
+\<^esub>                code: 0x0021d9  group: control  abbrev: =_)
+\<^bsup>                code: 0x0021d7  group: control  abbrev: =^(
+\<^esup>                code: 0x0021d6  group: control  abbrev: =^)
+\<^bold>                code: 0x002759  group: control  abbrev: -.