etc/symbols
author hoelzl
Mon, 08 Aug 2016 14:13:14 +0200
changeset 63627 6ddb43c6b711
parent 62440 31fa592761da
child 63677 be8b557ec73e
permissions -rw-r--r--
rename HOL-Multivariate_Analysis to HOL-Analysis.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27898
e0953043ce90 Default interpretation of some Isabelle symbols.
wenzelm
parents:
diff changeset
     1
# Default interpretation of some Isabelle symbols
e0953043ce90 Default interpretation of some Isabelle symbols.
wenzelm
parents:
diff changeset
     2
50188
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
     3
\<zero>                 code: 0x01d7ec  group: digit
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
     4
\<one>                  code: 0x01d7ed  group: digit
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
     5
\<two>                  code: 0x01d7ee  group: digit
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
     6
\<three>                code: 0x01d7ef  group: digit
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
     7
\<four>                 code: 0x01d7f0  group: digit
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
     8
\<five>                 code: 0x01d7f1  group: digit
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
     9
\<six>                  code: 0x01d7f2  group: digit
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
    10
\<seven>                code: 0x01d7f3  group: digit
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
    11
\<eight>                code: 0x01d7f4  group: digit
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
    12
\<nine>                 code: 0x01d7f5  group: digit
50137
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    13
\<A>                    code: 0x01d49c  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    14
\<B>                    code: 0x00212c  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    15
\<C>                    code: 0x01d49e  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    16
\<D>                    code: 0x01d49f  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    17
\<E>                    code: 0x002130  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    18
\<F>                    code: 0x002131  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    19
\<G>                    code: 0x01d4a2  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    20
\<H>                    code: 0x00210b  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    21
\<I>                    code: 0x002110  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    22
\<J>                    code: 0x01d4a5  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    23
\<K>                    code: 0x01d4a6  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    24
\<L>                    code: 0x002112  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    25
\<M>                    code: 0x002133  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    26
\<N>                    code: 0x01d4a9  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    27
\<O>                    code: 0x01d4aa  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    28
\<P>                    code: 0x01d4ab  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    29
\<Q>                    code: 0x01d4ac  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    30
\<R>                    code: 0x00211b  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    31
\<S>                    code: 0x01d4ae  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    32
\<T>                    code: 0x01d4af  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    33
\<U>                    code: 0x01d4b0  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    34
\<V>                    code: 0x01d4b1  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    35
\<W>                    code: 0x01d4b2  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    36
\<X>                    code: 0x01d4b3  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    37
\<Y>                    code: 0x01d4b4  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    38
\<Z>                    code: 0x01d4b5  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    39
\<a>                    code: 0x01d5ba  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    40
\<b>                    code: 0x01d5bb  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    41
\<c>                    code: 0x01d5bc  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    42
\<d>                    code: 0x01d5bd  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    43
\<e>                    code: 0x01d5be  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    44
\<f>                    code: 0x01d5bf  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    45
\<g>                    code: 0x01d5c0  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    46
\<h>                    code: 0x01d5c1  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    47
\<i>                    code: 0x01d5c2  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    48
\<j>                    code: 0x01d5c3  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    49
\<k>                    code: 0x01d5c4  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    50
\<l>                    code: 0x01d5c5  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    51
\<m>                    code: 0x01d5c6  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    52
\<n>                    code: 0x01d5c7  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    53
\<o>                    code: 0x01d5c8  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    54
\<p>                    code: 0x01d5c9  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    55
\<q>                    code: 0x01d5ca  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    56
\<r>                    code: 0x01d5cb  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    57
\<s>                    code: 0x01d5cc  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    58
\<t>                    code: 0x01d5cd  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    59
\<u>                    code: 0x01d5ce  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    60
\<v>                    code: 0x01d5cf  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    61
\<w>                    code: 0x01d5d0  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    62
\<x>                    code: 0x01d5d1  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    63
\<y>                    code: 0x01d5d2  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    64
\<z>                    code: 0x01d5d3  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    65
\<AA>                   code: 0x01d504  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    66
\<BB>                   code: 0x01d505  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    67
\<CC>                   code: 0x00212d  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    68
\<DD>                   code: 0x01d507  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    69
\<EE>                   code: 0x01d508  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    70
\<FF>                   code: 0x01d509  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    71
\<GG>                   code: 0x01d50a  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    72
\<HH>                   code: 0x00210c  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    73
\<II>                   code: 0x002111  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    74
\<JJ>                   code: 0x01d50d  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    75
\<KK>                   code: 0x01d50e  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    76
\<LL>                   code: 0x01d50f  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    77
\<MM>                   code: 0x01d510  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    78
\<NN>                   code: 0x01d511  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    79
\<OO>                   code: 0x01d512  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    80
\<PP>                   code: 0x01d513  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    81
\<QQ>                   code: 0x01d514  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    82
\<RR>                   code: 0x00211c  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    83
\<SS>                   code: 0x01d516  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    84
\<TT>                   code: 0x01d517  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    85
\<UU>                   code: 0x01d518  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    86
\<VV>                   code: 0x01d519  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    87
\<WW>                   code: 0x01d51a  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    88
\<XX>                   code: 0x01d51b  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    89
\<YY>                   code: 0x01d51c  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    90
\<ZZ>                   code: 0x002128  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    91
\<aa>                   code: 0x01d51e  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    92
\<bb>                   code: 0x01d51f  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    93
\<cc>                   code: 0x01d520  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    94
\<dd>                   code: 0x01d521  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    95
\<ee>                   code: 0x01d522  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    96
\<ff>                   code: 0x01d523  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    97
\<gg>                   code: 0x01d524  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    98
\<hh>                   code: 0x01d525  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
    99
\<ii>                   code: 0x01d526  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   100
\<jj>                   code: 0x01d527  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   101
\<kk>                   code: 0x01d528  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   102
\<ll>                   code: 0x01d529  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   103
\<mm>                   code: 0x01d52a  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   104
\<nn>                   code: 0x01d52b  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   105
\<oo>                   code: 0x01d52c  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   106
\<pp>                   code: 0x01d52d  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   107
\<qq>                   code: 0x01d52e  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   108
\<rr>                   code: 0x01d52f  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   109
\<ss>                   code: 0x01d530  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   110
\<tt>                   code: 0x01d531  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   111
\<uu>                   code: 0x01d532  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   112
\<vv>                   code: 0x01d533  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   113
\<ww>                   code: 0x01d534  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   114
\<xx>                   code: 0x01d535  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   115
\<yy>                   code: 0x01d536  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   116
\<zz>                   code: 0x01d537  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   117
\<alpha>                code: 0x0003b1  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   118
\<beta>                 code: 0x0003b2  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   119
\<gamma>                code: 0x0003b3  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   120
\<delta>                code: 0x0003b4  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   121
\<epsilon>              code: 0x0003b5  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   122
\<zeta>                 code: 0x0003b6  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   123
\<eta>                  code: 0x0003b7  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   124
\<theta>                code: 0x0003b8  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   125
\<iota>                 code: 0x0003b9  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   126
\<kappa>                code: 0x0003ba  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   127
\<lambda>               code: 0x0003bb  group: greek  abbrev: %
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   128
\<mu>                   code: 0x0003bc  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   129
\<nu>                   code: 0x0003bd  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   130
\<xi>                   code: 0x0003be  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   131
\<pi>                   code: 0x0003c0  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   132
\<rho>                  code: 0x0003c1  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   133
\<sigma>                code: 0x0003c3  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   134
\<tau>                  code: 0x0003c4  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   135
\<upsilon>              code: 0x0003c5  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   136
\<phi>                  code: 0x0003c6  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   137
\<chi>                  code: 0x0003c7  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   138
\<psi>                  code: 0x0003c8  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   139
\<omega>                code: 0x0003c9  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   140
\<Gamma>                code: 0x000393  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   141
\<Delta>                code: 0x000394  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   142
\<Theta>                code: 0x000398  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   143
\<Lambda>               code: 0x00039b  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   144
\<Xi>                   code: 0x00039e  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   145
\<Pi>                   code: 0x0003a0  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   146
\<Sigma>                code: 0x0003a3  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   147
\<Upsilon>              code: 0x0003a5  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   148
\<Phi>                  code: 0x0003a6  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   149
\<Psi>                  code: 0x0003a8  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   150
\<Omega>                code: 0x0003a9  group: greek
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   151
\<bool>                 code: 0x01d539  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   152
\<complex>              code: 0x002102  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   153
\<nat>                  code: 0x002115  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   154
\<rat>                  code: 0x00211a  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   155
\<real>                 code: 0x00211d  group: letter
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   156
\<int>                  code: 0x002124  group: letter
56443
ee0f7cfb7bba removed abbrev "<-" again (see c771f0fe28d1) due to conflict with important "<->" and "<-->";
wenzelm
parents: 56388
diff changeset
   157
\<leftarrow>            code: 0x002190  group: arrow  abbrev: <.
53345
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   158
\<longleftarrow>        code: 0x0027f5  group: arrow  abbrev: <.
61963
2548e7cc86fb more arrow symbols;
wenzelm
parents: 61653
diff changeset
   159
\<longlongleftarrow>    code: 0x00290e  group: arrow  abbrev: <.
2548e7cc86fb more arrow symbols;
wenzelm
parents: 61653
diff changeset
   160
\<longlonglongleftarrow> code: 0x0021e0 group: arrow  abbrev: <.
53345
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   161
\<rightarrow>           code: 0x002192  group: arrow  abbrev: .>  abbrev: ->
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   162
\<longrightarrow>       code: 0x0027f6  group: arrow  abbrev: .>  abbrev: -->
61963
2548e7cc86fb more arrow symbols;
wenzelm
parents: 61653
diff changeset
   163
\<longlongrightarrow>   code: 0x00290f  group: arrow  abbrev: .>  abbrev: --->
61972
a70b89a3e02e simplified abbrevs: exploit ambiguity;
wenzelm
parents: 61964
diff changeset
   164
\<longlonglongrightarrow> code: 0x0021e2 group: arrow abbrev: .>  abbrev: --->
53345
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   165
\<Leftarrow>            code: 0x0021d0  group: arrow  abbrev: <.
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   166
\<Longleftarrow>        code: 0x0027f8  group: arrow  abbrev: <.
61964
37a0cbee00c2 more arrow symbols;
wenzelm
parents: 61963
diff changeset
   167
\<Lleftarrow>           code: 0x0021da  group: arrow  abbrev: <.
53345
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   168
\<Rightarrow>           code: 0x0021d2  group: arrow  abbrev: .>  abbrev: =>
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   169
\<Longrightarrow>       code: 0x0027f9  group: arrow  abbrev: .>  abbrev: ==>
61964
37a0cbee00c2 more arrow symbols;
wenzelm
parents: 61963
diff changeset
   170
\<Rrightarrow>          code: 0x0021db  group: arrow  abbrev: .>
53345
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   171
\<leftrightarrow>       code: 0x002194  group: arrow  abbrev: <>  abbrev: <->
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   172
\<longleftrightarrow>   code: 0x0027f7  group: arrow  abbrev: <>  abbrev: <->  abbrev: <-->
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   173
\<Leftrightarrow>       code: 0x0021d4  group: arrow  abbrev: <>
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   174
\<Longleftrightarrow>   code: 0x0027fa  group: arrow  abbrev: <>
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   175
\<mapsto>               code: 0x0021a6  group: arrow  abbrev: .>  abbrev: |->
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   176
\<longmapsto>           code: 0x0027fc  group: arrow  abbrev: .>  abbrev: |-->
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   177
\<midarrow>             code: 0x002500  group: arrow  abbrev: <>
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   178
\<Midarrow>             code: 0x002550  group: arrow  abbrev: <>
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   179
\<hookleftarrow>        code: 0x0021a9  group: arrow  abbrev: <.
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   180
\<hookrightarrow>       code: 0x0021aa  group: arrow  abbrev: .>
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   181
\<leftharpoondown>      code: 0x0021bd  group: arrow  abbrev: <.
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   182
\<rightharpoondown>     code: 0x0021c1  group: arrow  abbrev: .>
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   183
\<leftharpoonup>        code: 0x0021bc  group: arrow  abbrev: <.
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   184
\<rightharpoonup>       code: 0x0021c0  group: arrow  abbrev: .>
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   185
\<rightleftharpoons>    code: 0x0021cc  group: arrow  abbrev: <> abbrev: ==
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   186
\<leadsto>              code: 0x00219d  group: arrow  abbrev: .> abbrev: ~>
50137
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   187
\<downharpoonleft>      code: 0x0021c3  group: arrow
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   188
\<downharpoonright>     code: 0x0021c2  group: arrow
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   189
\<upharpoonleft>        code: 0x0021bf  group: arrow
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   190
#\<upharpoonright>       code: 0x0021be  group: arrow
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   191
\<restriction>          code: 0x0021be  group: punctuation
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   192
\<Colon>                code: 0x002237  group: punctuation
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   193
\<up>                   code: 0x002191  group: arrow
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   194
\<Up>                   code: 0x0021d1  group: arrow
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   195
\<down>                 code: 0x002193  group: arrow
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   196
\<Down>                 code: 0x0021d3  group: arrow
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   197
\<updown>               code: 0x002195  group: arrow
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   198
\<Updown>               code: 0x0021d5  group: arrow
53319
5f310fb79c62 misc tuning -- reduce conflicts;
wenzelm
parents: 53317
diff changeset
   199
\<langle>               code: 0x0027e8  group: punctuation  abbrev: <<
5f310fb79c62 misc tuning -- reduce conflicts;
wenzelm
parents: 53317
diff changeset
   200
\<rangle>               code: 0x0027e9  group: punctuation  abbrev: >>
53320
17b887110cc1 more symbol abbrevs;
wenzelm
parents: 53319
diff changeset
   201
\<lceil>                code: 0x002308  group: punctuation  abbrev: [.
17b887110cc1 more symbol abbrevs;
wenzelm
parents: 53319
diff changeset
   202
\<rceil>                code: 0x002309  group: punctuation  abbrev: .]
17b887110cc1 more symbol abbrevs;
wenzelm
parents: 53319
diff changeset
   203
\<lfloor>               code: 0x00230a  group: punctuation  abbrev: [.
17b887110cc1 more symbol abbrevs;
wenzelm
parents: 53319
diff changeset
   204
\<rfloor>               code: 0x00230b  group: punctuation  abbrev: .]
50137
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   205
\<lparr>                code: 0x002987  group: punctuation  abbrev: (|
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   206
\<rparr>                code: 0x002988  group: punctuation  abbrev: |)
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   207
\<lbrakk>               code: 0x0027e6  group: punctuation  abbrev: [|
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   208
\<rbrakk>               code: 0x0027e7  group: punctuation  abbrev: |]
53319
5f310fb79c62 misc tuning -- reduce conflicts;
wenzelm
parents: 53317
diff changeset
   209
\<lbrace>               code: 0x002983  group: punctuation  abbrev: {|
5f310fb79c62 misc tuning -- reduce conflicts;
wenzelm
parents: 53317
diff changeset
   210
\<rbrace>               code: 0x002984  group: punctuation  abbrev: |}
50137
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   211
\<guillemotleft>        code: 0x0000ab  group: punctuation  abbrev: <<
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   212
\<guillemotright>       code: 0x0000bb  group: punctuation  abbrev: >>
50188
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
   213
\<bottom>               code: 0x0022a5  group: logic
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
   214
\<top>                  code: 0x0022a4  group: logic
53317
dea84641ca35 more symbol abbrevs, based on ProofGeneral-4.2/isar/isar-unicode-tokens.el and traditional Isabelle/HOL ASCII replacement syntax;
wenzelm
parents: 53251
diff changeset
   215
\<and>                  code: 0x002227  group: logic  abbrev: /\  abbrev: &
50188
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
   216
\<And>                  code: 0x0022c0  group: logic  abbrev: !!
53317
dea84641ca35 more symbol abbrevs, based on ProofGeneral-4.2/isar/isar-unicode-tokens.el and traditional Isabelle/HOL ASCII replacement syntax;
wenzelm
parents: 53251
diff changeset
   217
\<or>                   code: 0x002228  group: logic  abbrev: \/  abbrev: |
50188
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
   218
\<Or>                   code: 0x0022c1  group: logic  abbrev: ??
53317
dea84641ca35 more symbol abbrevs, based on ProofGeneral-4.2/isar/isar-unicode-tokens.el and traditional Isabelle/HOL ASCII replacement syntax;
wenzelm
parents: 53251
diff changeset
   219
\<forall>               code: 0x002200  group: logic  abbrev: !  abbrev: ALL
dea84641ca35 more symbol abbrevs, based on ProofGeneral-4.2/isar/isar-unicode-tokens.el and traditional Isabelle/HOL ASCII replacement syntax;
wenzelm
parents: 53251
diff changeset
   220
\<exists>               code: 0x002203  group: logic  abbrev: ?  abbrev: EX
50188
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
   221
\<nexists>              code: 0x002204  group: logic  abbrev: ~?
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
   222
\<not>                  code: 0x0000ac  group: logic  abbrev: ~
62440
31fa592761da symbol interpretation for \<circle>;
wenzelm
parents: 62260
diff changeset
   223
\<circle>               code: 0x0025cb  group: logic
50188
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
   224
\<box>                  code: 0x0025a1  group: logic
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
   225
\<diamond>              code: 0x0025c7  group: logic
62108
0046bacc5f5b \<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents: 62025
diff changeset
   226
\<diamondop>            code: 0x0022c4  group: operator
50137
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   227
\<turnstile>            code: 0x0022a2  group: relation  abbrev: |-
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   228
\<Turnstile>            code: 0x0022a8  group: relation  abbrev: |=
53319
5f310fb79c62 misc tuning -- reduce conflicts;
wenzelm
parents: 53317
diff changeset
   229
\<tturnstile>           code: 0x0022a9  group: relation  abbrev: |-
5f310fb79c62 misc tuning -- reduce conflicts;
wenzelm
parents: 53317
diff changeset
   230
\<TTurnstile>           code: 0x0022ab  group: relation  abbrev: |=
50137
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   231
\<stileturn>            code: 0x0022a3  group: relation  abbrev: -|
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   232
\<surd>                 code: 0x00221a  group: relation
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   233
\<le>                   code: 0x002264  group: relation  abbrev: <=
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   234
\<ge>                   code: 0x002265  group: relation  abbrev: >=
53317
dea84641ca35 more symbol abbrevs, based on ProofGeneral-4.2/isar/isar-unicode-tokens.el and traditional Isabelle/HOL ASCII replacement syntax;
wenzelm
parents: 53251
diff changeset
   235
\<lless>                code: 0x00226a  group: relation  abbrev: <<
dea84641ca35 more symbol abbrevs, based on ProofGeneral-4.2/isar/isar-unicode-tokens.el and traditional Isabelle/HOL ASCII replacement syntax;
wenzelm
parents: 53251
diff changeset
   236
\<ggreater>             code: 0x00226b  group: relation  abbrev: >>
50137
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   237
\<lesssim>              code: 0x002272  group: relation
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   238
\<greatersim>           code: 0x002273  group: relation
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   239
\<lessapprox>           code: 0x002a85  group: relation
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   240
\<greaterapprox>        code: 0x002a86  group: relation
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   241
\<in>                   code: 0x002208  group: relation  abbrev: :
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   242
\<notin>                code: 0x002209  group: relation  abbrev: ~:
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   243
\<subset>               code: 0x002282  group: relation
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   244
\<supset>               code: 0x002283  group: relation
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   245
\<subseteq>             code: 0x002286  group: relation  abbrev: (=
53343
8dc406adbc75 added common alternative for == (its ambiguity also avoids conflict with ==>);
wenzelm
parents: 53323
diff changeset
   246
\<supseteq>             code: 0x002287  group: relation  abbrev: )=
50137
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   247
\<sqsubset>             code: 0x00228f  group: relation
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   248
\<sqsupset>             code: 0x002290  group: relation
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   249
\<sqsubseteq>           code: 0x002291  group: relation  abbrev: [=
53343
8dc406adbc75 added common alternative for == (its ambiguity also avoids conflict with ==>);
wenzelm
parents: 53323
diff changeset
   250
\<sqsupseteq>           code: 0x002292  group: relation  abbrev: ]=
53317
dea84641ca35 more symbol abbrevs, based on ProofGeneral-4.2/isar/isar-unicode-tokens.el and traditional Isabelle/HOL ASCII replacement syntax;
wenzelm
parents: 53251
diff changeset
   251
\<inter>                code: 0x002229  group: operator  abbrev: Int
53344
9a5eaa6b0154 more abbrevs according to Isabelle/HOL ASCII replacement syntax;
wenzelm
parents: 53343
diff changeset
   252
\<Inter>                code: 0x0022c2  group: operator  abbrev: Inter  abbrev: INT
53317
dea84641ca35 more symbol abbrevs, based on ProofGeneral-4.2/isar/isar-unicode-tokens.el and traditional Isabelle/HOL ASCII replacement syntax;
wenzelm
parents: 53251
diff changeset
   253
\<union>                code: 0x00222a  group: operator  abbrev: Un
53344
9a5eaa6b0154 more abbrevs according to Isabelle/HOL ASCII replacement syntax;
wenzelm
parents: 53343
diff changeset
   254
\<Union>                code: 0x0022c3  group: operator  abbrev: Union  abbrev: UN
50137
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   255
\<squnion>              code: 0x002294  group: operator
53317
dea84641ca35 more symbol abbrevs, based on ProofGeneral-4.2/isar/isar-unicode-tokens.el and traditional Isabelle/HOL ASCII replacement syntax;
wenzelm
parents: 53251
diff changeset
   256
\<Squnion>              code: 0x002a06  group: operator  abbrev: SUP
50137
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   257
\<sqinter>              code: 0x002293  group: operator
53317
dea84641ca35 more symbol abbrevs, based on ProofGeneral-4.2/isar/isar-unicode-tokens.el and traditional Isabelle/HOL ASCII replacement syntax;
wenzelm
parents: 53251
diff changeset
   258
\<Sqinter>              code: 0x002a05  group: operator  abbrev: INF
50137
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   259
\<setminus>             code: 0x002216  group: operator
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   260
\<propto>               code: 0x00221d  group: operator
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   261
\<uplus>                code: 0x00228e  group: operator
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   262
\<Uplus>                code: 0x002a04  group: operator
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   263
\<noteq>                code: 0x002260  group: relation  abbrev: ~=
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   264
\<sim>                  code: 0x00223c  group: relation
53319
5f310fb79c62 misc tuning -- reduce conflicts;
wenzelm
parents: 53317
diff changeset
   265
\<doteq>                code: 0x002250  group: relation  abbrev: .=
50137
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   266
\<simeq>                code: 0x002243  group: relation
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   267
\<approx>               code: 0x002248  group: relation
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   268
\<asymp>                code: 0x00224d  group: relation
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   269
\<cong>                 code: 0x002245  group: relation
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   270
\<smile>                code: 0x002323  group: relation
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   271
\<equiv>                code: 0x002261  group: relation  abbrev: ==
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   272
\<frown>                code: 0x002322  group: relation
43486
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   273
\<Join>                 code: 0x0022c8
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   274
\<bowtie>               code: 0x002a1d
50137
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   275
\<prec>                 code: 0x00227a  group: relation
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   276
\<succ>                 code: 0x00227b  group: relation
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   277
\<preceq>               code: 0x00227c  group: relation
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   278
\<succeq>               code: 0x00227d  group: relation
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   279
\<parallel>             code: 0x002225  group: punctuation  abbrev: ||
53320
17b887110cc1 more symbol abbrevs;
wenzelm
parents: 53319
diff changeset
   280
\<bar>                  code: 0x0000a6  group: punctuation  abbrev: ||
50137
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   281
\<plusminus>            code: 0x0000b1  group: operator
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   282
\<minusplus>            code: 0x002213  group: operator
55786
96861130f922 more symbol abbrevs to support HOL library maintenance;
wenzelm
parents: 55546
diff changeset
   283
\<times>                code: 0x0000d7  group: operator  abbrev: <*>
50137
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   284
\<div>                  code: 0x0000f7  group: operator
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   285
\<cdot>                 code: 0x0022c5  group: operator
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   286
\<star>                 code: 0x0022c6  group: operator
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   287
\<bullet>               code: 0x002219  group: operator
53323
5fa77d6ad63d single-letter abbrev does not make sense -- too many candidates;
wenzelm
parents: 53321
diff changeset
   288
\<circ>                 code: 0x002218  group: operator
43486
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   289
\<dagger>               code: 0x002020
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   290
\<ddagger>              code: 0x002021
50137
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   291
\<lhd>                  code: 0x0022b2  group: relation
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   292
\<rhd>                  code: 0x0022b3  group: relation
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   293
\<unlhd>                code: 0x0022b4  group: relation
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   294
\<unrhd>                code: 0x0022b5  group: relation
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   295
\<triangleleft>         code: 0x0025c3  group: relation
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   296
\<triangleright>        code: 0x0025b9  group: relation
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   297
\<triangle>             code: 0x0025b3  group: relation
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   298
\<triangleq>            code: 0x00225c  group: relation
62234
7cc9d7b822ae discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "-o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;
wenzelm
parents: 62108
diff changeset
   299
\<oplus>                code: 0x002295  group: operator
7cc9d7b822ae discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "-o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;
wenzelm
parents: 62108
diff changeset
   300
\<Oplus>                code: 0x002a01  group: operator
7cc9d7b822ae discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "-o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;
wenzelm
parents: 62108
diff changeset
   301
\<otimes>               code: 0x002297  group: operator
7cc9d7b822ae discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "-o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;
wenzelm
parents: 62108
diff changeset
   302
\<Otimes>               code: 0x002a02  group: operator
7cc9d7b822ae discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "-o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;
wenzelm
parents: 62108
diff changeset
   303
\<odot>                 code: 0x002299  group: operator
7cc9d7b822ae discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "-o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;
wenzelm
parents: 62108
diff changeset
   304
\<Odot>                 code: 0x002a00  group: operator
7cc9d7b822ae discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "-o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;
wenzelm
parents: 62108
diff changeset
   305
\<ominus>               code: 0x002296  group: operator
7cc9d7b822ae discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "-o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;
wenzelm
parents: 62108
diff changeset
   306
\<oslash>               code: 0x002298  group: operator
50188
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
   307
\<dots>                 code: 0x002026  group: punctuation abbrev: ...
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
   308
\<cdots>                code: 0x0022ef  group: punctuation
50137
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   309
\<Sum>                  code: 0x002211  group: operator  abbrev: SUM
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   310
\<Prod>                 code: 0x00220f  group: operator  abbrev: PROD
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   311
\<Coprod>               code: 0x002210  group: operator
43486
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   312
\<infinity>             code: 0x00221e
50137
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   313
\<integral>             code: 0x00222b  group: operator
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   314
\<ointegral>            code: 0x00222e  group: operator
43486
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   315
\<clubsuit>             code: 0x002663
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   316
\<diamondsuit>          code: 0x002662
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   317
\<heartsuit>            code: 0x002661
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   318
\<spadesuit>            code: 0x002660
50193
3ef3e3e75166 tuned symbol groups;
wenzelm
parents: 50188
diff changeset
   319
\<aleph>                code: 0x002135
43486
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   320
\<emptyset>             code: 0x002205
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   321
\<nabla>                code: 0x002207
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   322
\<partial>              code: 0x002202
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   323
\<flat>                 code: 0x00266d
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   324
\<natural>              code: 0x00266e
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   325
\<sharp>                code: 0x00266f
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   326
\<angle>                code: 0x002220
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   327
\<copyright>            code: 0x0000a9
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   328
\<registered>           code: 0x0000ae
50137
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   329
\<hyphen>               code: 0x0000ad  group: punctuation
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   330
\<inverse>              code: 0x0000af  group: punctuation
50188
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
   331
\<onequarter>           code: 0x0000bc  group: digit
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
   332
\<onehalf>              code: 0x0000bd  group: digit
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
   333
\<threequarters>        code: 0x0000be  group: digit
27899
a152c8a38b7d removed redundant "symbol" property;
wenzelm
parents: 27898
diff changeset
   334
\<ordfeminine>          code: 0x0000aa
a152c8a38b7d removed redundant "symbol" property;
wenzelm
parents: 27898
diff changeset
   335
\<ordmasculine>         code: 0x0000ba
a152c8a38b7d removed redundant "symbol" property;
wenzelm
parents: 27898
diff changeset
   336
\<section>              code: 0x0000a7
61592
d80eb8f6eb47 retain traditional rendering of \<paragraph>;
wenzelm
parents: 61584
diff changeset
   337
\<paragraph>            code: 0x0000b6
27899
a152c8a38b7d removed redundant "symbol" property;
wenzelm
parents: 27898
diff changeset
   338
\<exclamdown>           code: 0x0000a1
a152c8a38b7d removed redundant "symbol" property;
wenzelm
parents: 27898
diff changeset
   339
\<questiondown>         code: 0x0000bf
27900
fdd6e68e29d9 added some abbrevs;
wenzelm
parents: 27899
diff changeset
   340
\<euro>                 code: 0x0020ac
27899
a152c8a38b7d removed redundant "symbol" property;
wenzelm
parents: 27898
diff changeset
   341
\<pounds>               code: 0x0000a3
a152c8a38b7d removed redundant "symbol" property;
wenzelm
parents: 27898
diff changeset
   342
\<yen>                  code: 0x0000a5
a152c8a38b7d removed redundant "symbol" property;
wenzelm
parents: 27898
diff changeset
   343
\<cent>                 code: 0x0000a2
a152c8a38b7d removed redundant "symbol" property;
wenzelm
parents: 27898
diff changeset
   344
\<currency>             code: 0x0000a4
43486
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   345
\<degree>               code: 0x0000b0
50137
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   346
\<amalg>                code: 0x002a3f  group: operator
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   347
\<mho>                  code: 0x002127  group: operator
43486
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   348
\<lozenge>              code: 0x0025ca
50193
3ef3e3e75166 tuned symbol groups;
wenzelm
parents: 50188
diff changeset
   349
\<wp>                   code: 0x002118
50137
0226d408058b some grouping of Isabelle symbols, based on X-Symbol grid in PG-3.7.1.1 and a proposal by Fabian Immler;
wenzelm
parents: 48670
diff changeset
   350
\<wrong>                code: 0x002240  group: relation
27899
a152c8a38b7d removed redundant "symbol" property;
wenzelm
parents: 27898
diff changeset
   351
\<acute>                code: 0x0000b4
43486
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   352
\<index>                code: 0x000131
27899
a152c8a38b7d removed redundant "symbol" property;
wenzelm
parents: 27898
diff changeset
   353
\<dieresis>             code: 0x0000a8
a152c8a38b7d removed redundant "symbol" property;
wenzelm
parents: 27898
diff changeset
   354
\<cedilla>              code: 0x0000b8
a152c8a38b7d removed redundant "symbol" property;
wenzelm
parents: 27898
diff changeset
   355
\<hungarumlaut>         code: 0x0002dd
62025
8007e4ff493a clarified abbrev;
wenzelm
parents: 62023
diff changeset
   356
\<bind>                 code: 0x00291c  abbrev: >>=
62022
7a6ae107ec3c glyphs for \<bind>, \<then>;
wenzelm
parents: 61972
diff changeset
   357
\<then>                 code: 0x002aa2  abbrev: >>
43486
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   358
\<some>                 code: 0x0003f5
59974
b911c8ba0b69 added symbol for \<hole> (from DejaVuSansMono and DejaVuSansMono-Bold version 2.34);
wenzelm
parents: 57081
diff changeset
   359
\<hole>                 code: 0x002311
55015
e33c5bd729ff added \<newline> symbol, which is used for char/string literals in HOL;
wenzelm
parents: 53345
diff changeset
   360
\<newline>              code: 0x0023ce
62260
f82f6c7476a1 clarified;
wenzelm
parents: 62234
diff changeset
   361
\<comment>              code: 0x002015  group: document  font: IsabelleText
57081
5fc1c2098964 receovered alternative abbrevs for \<open> \<close> from 8e8243975860, to accommodate national keyboard layouts where "`" might be hard to produce;
wenzelm
parents: 56591
diff changeset
   362
\<open>                 code: 0x002039  group: punctuation  font: IsabelleText  abbrev: <<
5fc1c2098964 receovered alternative abbrevs for \<open> \<close> from 8e8243975860, to accommodate national keyboard layouts where "`" might be hard to produce;
wenzelm
parents: 56591
diff changeset
   363
\<close>                code: 0x00203a  group: punctuation  font: IsabelleText  abbrev: >>
55546
76979adf0b96 always show PIDE positions as \<here> (0x002302 "House" from DejaVuSansMono);
wenzelm
parents: 55044
diff changeset
   364
\<here>                 code: 0x002302  font: IsabelleText
62023
19605292757e clarified groups, notably for Symbols dockable;
wenzelm
parents: 62022
diff changeset
   365
\<^undefined>           code: 0x002756  font: IsabelleText
19605292757e clarified groups, notably for Symbols dockable;
wenzelm
parents: 62022
diff changeset
   366
\<^noindent>            code: 0x0021e4  group: document  font: IsabelleText
19605292757e clarified groups, notably for Symbols dockable;
wenzelm
parents: 62022
diff changeset
   367
\<^smallskip>           code: 0x002508  group: document  font: IsabelleText
19605292757e clarified groups, notably for Symbols dockable;
wenzelm
parents: 62022
diff changeset
   368
\<^medskip>             code: 0x002509  group: document  font: IsabelleText
19605292757e clarified groups, notably for Symbols dockable;
wenzelm
parents: 62022
diff changeset
   369
\<^bigskip>             code: 0x002501  group: document  font: IsabelleText
19605292757e clarified groups, notably for Symbols dockable;
wenzelm
parents: 62022
diff changeset
   370
\<^item>                code: 0x0025aa  group: document  font: IsabelleText
19605292757e clarified groups, notably for Symbols dockable;
wenzelm
parents: 62022
diff changeset
   371
\<^enum>                code: 0x0025b8  group: document  font: IsabelleText
19605292757e clarified groups, notably for Symbols dockable;
wenzelm
parents: 62022
diff changeset
   372
\<^descr>               code: 0x0027a7  group: document  font: IsabelleText
19605292757e clarified groups, notably for Symbols dockable;
wenzelm
parents: 62022
diff changeset
   373
\<^footnote>            code: 0x00204b  group: document  font: IsabelleText
19605292757e clarified groups, notably for Symbols dockable;
wenzelm
parents: 62022
diff changeset
   374
\<^verbatim>            code: 0x0025a9  group: document  font: IsabelleText
19605292757e clarified groups, notably for Symbols dockable;
wenzelm
parents: 62022
diff changeset
   375
\<^theory_text>         code: 0x002b1a  group: document  font: IsabelleText
19605292757e clarified groups, notably for Symbols dockable;
wenzelm
parents: 62022
diff changeset
   376
\<^emph>                code: 0x002217  group: document  font: IsabelleText
19605292757e clarified groups, notably for Symbols dockable;
wenzelm
parents: 62022
diff changeset
   377
\<^bold>                code: 0x002759  group: control  group: document  font: IsabelleText
53073
1835a83309d6 discontinued redundant abbreviations -- Isabelle/jEdit provides keyboard shortcuts already;
wenzelm
parents: 53021
diff changeset
   378
\<^sub>                 code: 0x0021e9  group: control  font: IsabelleText
1835a83309d6 discontinued redundant abbreviations -- Isabelle/jEdit provides keyboard shortcuts already;
wenzelm
parents: 53021
diff changeset
   379
\<^sup>                 code: 0x0021e7  group: control  font: IsabelleText
50194
829ce6e03279 more robust font for control symbols, to ensure these obscure codepoints are properly rendered;
wenzelm
parents: 50193
diff changeset
   380
\<^bsub>                code: 0x0021d8  group: control_block  font: IsabelleText  abbrev: =_(
829ce6e03279 more robust font for control symbols, to ensure these obscure codepoints are properly rendered;
wenzelm
parents: 50193
diff changeset
   381
\<^esub>                code: 0x0021d9  group: control_block  font: IsabelleText  abbrev: =_)
829ce6e03279 more robust font for control symbols, to ensure these obscure codepoints are properly rendered;
wenzelm
parents: 50193
diff changeset
   382
\<^bsup>                code: 0x0021d7  group: control_block  font: IsabelleText  abbrev: =^(
829ce6e03279 more robust font for control symbols, to ensure these obscure codepoints are properly rendered;
wenzelm
parents: 50193
diff changeset
   383
\<^esup>                code: 0x0021d6  group: control_block  font: IsabelleText  abbrev: =^)