etc/symbols
author haftmann
Fri, 14 Jun 2019 08:34:27 +0000
changeset 70335 9bd8c16b6627
parent 70204 230188a56a9e
child 70368 b67737bc5bd1
permissions -rw-r--r--
using (*)-syntax for partially applied infix is fine, contrary to ancient op-syntax
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
69361
0d84e3db67c2 clarified symbol groups;
wenzelm
parents: 69343
diff changeset
   191
\<restriction>          code: 0x0021be  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
   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
67305
ecb74607063f more robust hyphen (see also "Soft hyphen (SHY) – a hard problem?" http://jkorpela.fi/shy.html);
wenzelm
parents: 64556
diff changeset
   329
\<hyphen>               code: 0x002010  group: punctuation
69361
0d84e3db67c2 clarified symbol groups;
wenzelm
parents: 69343
diff changeset
   330
\<inverse>              code: 0x0000af  group: operator
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
69361
0d84e3db67c2 clarified symbol groups;
wenzelm
parents: 69343
diff changeset
   356
\<bind>                 code: 0x00291c  group: operator  abbrev: >>=
0d84e3db67c2 clarified symbol groups;
wenzelm
parents: 69343
diff changeset
   357
\<then>                 code: 0x002aa2  group: operator  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
69343
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   361
\<comment>              code: 0x002015  group: document  argument: space_cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   362
\<^cancel>              code: 0x002326  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
67430
149b742070e9 support for completion;
wenzelm
parents: 67424
diff changeset
   363
\<^latex>                               group: document  argument: cartouche
69891
def3ec9cdb7e document markers are formal comments, and may thus occur anywhere in the command-span;
wenzelm
parents: 69885
diff changeset
   364
\<^marker>              code: 0x002710  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
69343
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   365
\<open>                 code: 0x002039  group: punctuation  font: Isabelle␣DejaVu␣Sans␣Mono  abbrev: <<
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   366
\<close>                code: 0x00203a  group: punctuation  font: Isabelle␣DejaVu␣Sans␣Mono  abbrev: >>
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   367
\<^here>                code: 0x002302  font: Isabelle␣DejaVu␣Sans␣Mono
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   368
\<^undefined>           code: 0x002756  font: Isabelle␣DejaVu␣Sans␣Mono
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   369
\<^noindent>            code: 0x0021e4  group: document  font: Isabelle␣DejaVu␣Sans␣Mono
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   370
\<^smallskip>           code: 0x002508  group: document  font: Isabelle␣DejaVu␣Sans␣Mono
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   371
\<^medskip>             code: 0x002509  group: document  font: Isabelle␣DejaVu␣Sans␣Mono
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   372
\<^bigskip>             code: 0x002501  group: document  font: Isabelle␣DejaVu␣Sans␣Mono
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   373
\<^item>                code: 0x0025aa  group: document  font: Isabelle␣DejaVu␣Sans␣Mono
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   374
\<^enum>                code: 0x0025b8  group: document  font: Isabelle␣DejaVu␣Sans␣Mono
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   375
\<^descr>               code: 0x0027a7  group: document  font: Isabelle␣DejaVu␣Sans␣Mono
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   376
\<^footnote>            code: 0x00204b  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   377
\<^verbatim>            code: 0x0025a9  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   378
\<^theory_text>         code: 0x002b1a  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   379
\<^emph>                code: 0x002217  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   380
\<^bold>                code: 0x002759  group: control  argument: cartouche  group: document  font: Isabelle␣DejaVu␣Sans␣Mono
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   381
\<^sub>                 code: 0x0021e9  group: control  font: Isabelle␣DejaVu␣Sans␣Mono
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   382
\<^sup>                 code: 0x0021e7  group: control  font: Isabelle␣DejaVu␣Sans␣Mono
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   383
\<^bsub>                code: 0x0021d8  group: control_block  font: Isabelle␣DejaVu␣Sans␣Mono  abbrev: =_(
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   384
\<^esub>                code: 0x0021d9  group: control_block  font: Isabelle␣DejaVu␣Sans␣Mono  abbrev: =_)
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   385
\<^bsup>                code: 0x0021d7  group: control_block  font: Isabelle␣DejaVu␣Sans␣Mono  abbrev: =^(
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   386
\<^esup>                code: 0x0021d6  group: control_block  font: Isabelle␣DejaVu␣Sans␣Mono  abbrev: =^)
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   387
\<^file>                code: 0x01F5CF  group: icon  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   388
\<^dir>                 code: 0x01F5C0  group: icon  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   389
\<^url>                 code: 0x01F310  group: icon  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   390
\<^doc>                 code: 0x01F4D3  group: icon  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   391
\<^action>              code: 0x00261b  group: icon  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
67311
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   392
\<^assert>
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   393
\<^binding>             argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   394
\<^class>               argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   395
\<^class_syntax>        argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   396
\<^command_keyword>     argument: cartouche
70204
230188a56a9e completion for \<^const>, although it often requires an extra argument;
wenzelm
parents: 70015
diff changeset
   397
\<^const>               argument: cartouche
67311
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   398
\<^const_abbrev>        argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   399
\<^const_name>          argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   400
\<^const_syntax>        argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   401
\<^context>
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   402
\<^cprop>               argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   403
\<^cterm>               argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   404
\<^ctyp>                argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   405
\<^keyword>             argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   406
\<^locale>              argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   407
\<^make_string>
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   408
\<^method>              argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   409
\<^named_theorems>      argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   410
\<^nonterminal>         argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   411
\<^path>                argument: cartouche
70015
c8e08d8ffb93 clarified signature: more explicit type Path.binding;
wenzelm
parents: 69891
diff changeset
   412
\<^path_binding>        argument: cartouche
67311
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   413
\<^plugin>              argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   414
\<^print>
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   415
\<^prop>                argument: cartouche
67470
d36fcde7e2c0 support for completion;
wenzelm
parents: 67430
diff changeset
   416
\<^session>             argument: cartouche
67311
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   417
\<^simproc>             argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   418
\<^sort>                argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   419
\<^syntax_const>        argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   420
\<^system_option>       argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   421
\<^term>                argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   422
\<^theory>              argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   423
\<^theory_context>      argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   424
\<^typ>                 argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   425
\<^type_abbrev>         argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   426
\<^type_name>           argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   427
\<^type_syntax>         argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   428
\<^code>                argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   429
\<^computation>         argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   430
\<^computation_conv>    argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   431
\<^computation_check>   argument: cartouche