etc/symbols
author wenzelm
Sat, 16 Oct 2021 20:21:13 +0200
changeset 74532 64d1b02327a4
parent 74433 ec1774613824
child 74568 7f311d474cf9
permissions -rw-r--r--
more accurate treatment of context; declare generated bounds for the sake of recdef, which has variables leaking from local context;
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
73461
067c23324784 clarified symbol names, notably relevant for Z_Notation;
wenzelm
parents: 73459
diff changeset
   151
\<bbbA>                 code: 0x01D538  group: letter  group: Z_Notation
73450
c5315b89c1bf more Z_Notation symbols, as proposed by Simon Foster;
wenzelm
parents: 73447
diff changeset
   152
\<bool>                 code: 0x01d539  group: letter  group: Z_Notation
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
   153
\<complex>              code: 0x002102  group: letter
73459
1f1f4462a6ae high-quality blackboard-bold fonts from "txmia" (package "txfonts");
wenzelm
parents: 73457
diff changeset
   154
\<bbbD>                 code: 0x01D53B  group: letter
1f1f4462a6ae high-quality blackboard-bold fonts from "txmia" (package "txfonts");
wenzelm
parents: 73457
diff changeset
   155
\<bbbE>                 code: 0x01D53C  group: letter
73461
067c23324784 clarified symbol names, notably relevant for Z_Notation;
wenzelm
parents: 73459
diff changeset
   156
\<bbbF>                 code: 0x01D53D  group: letter  group: Z_Notation
73459
1f1f4462a6ae high-quality blackboard-bold fonts from "txmia" (package "txfonts");
wenzelm
parents: 73457
diff changeset
   157
\<bbbG>                 code: 0x01D53E  group: letter
1f1f4462a6ae high-quality blackboard-bold fonts from "txmia" (package "txfonts");
wenzelm
parents: 73457
diff changeset
   158
\<bbbH>                 code: 0x00210D  group: letter
1f1f4462a6ae high-quality blackboard-bold fonts from "txmia" (package "txfonts");
wenzelm
parents: 73457
diff changeset
   159
\<bbbI>                 code: 0x01D540  group: letter
1f1f4462a6ae high-quality blackboard-bold fonts from "txmia" (package "txfonts");
wenzelm
parents: 73457
diff changeset
   160
\<bbbJ>                 code: 0x01D541  group: letter
1f1f4462a6ae high-quality blackboard-bold fonts from "txmia" (package "txfonts");
wenzelm
parents: 73457
diff changeset
   161
\<bbbK>                 code: 0x01D542  group: letter
1f1f4462a6ae high-quality blackboard-bold fonts from "txmia" (package "txfonts");
wenzelm
parents: 73457
diff changeset
   162
\<bbbL>                 code: 0x01D543  group: letter
1f1f4462a6ae high-quality blackboard-bold fonts from "txmia" (package "txfonts");
wenzelm
parents: 73457
diff changeset
   163
\<bbbM>                 code: 0x01D544  group: letter
73450
c5315b89c1bf more Z_Notation symbols, as proposed by Simon Foster;
wenzelm
parents: 73447
diff changeset
   164
\<nat>                  code: 0x002115  group: letter  group: Z_Notation
73459
1f1f4462a6ae high-quality blackboard-bold fonts from "txmia" (package "txfonts");
wenzelm
parents: 73457
diff changeset
   165
\<bbbO>                 code: 0x01D546  group: letter
73461
067c23324784 clarified symbol names, notably relevant for Z_Notation;
wenzelm
parents: 73459
diff changeset
   166
\<bbbP>                 code: 0x002119  group: letter  group: Z_Notation
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
   167
\<rat>                  code: 0x00211a  group: letter
73450
c5315b89c1bf more Z_Notation symbols, as proposed by Simon Foster;
wenzelm
parents: 73447
diff changeset
   168
\<real>                 code: 0x00211d  group: letter  group: Z_Notation
73459
1f1f4462a6ae high-quality blackboard-bold fonts from "txmia" (package "txfonts");
wenzelm
parents: 73457
diff changeset
   169
\<bbbS>                 code: 0x01D54A  group: letter
1f1f4462a6ae high-quality blackboard-bold fonts from "txmia" (package "txfonts");
wenzelm
parents: 73457
diff changeset
   170
\<bbbT>                 code: 0x01D54B  group: letter
73461
067c23324784 clarified symbol names, notably relevant for Z_Notation;
wenzelm
parents: 73459
diff changeset
   171
\<bbbU>                 code: 0x01D54C  group: letter  group: Z_Notation
73459
1f1f4462a6ae high-quality blackboard-bold fonts from "txmia" (package "txfonts");
wenzelm
parents: 73457
diff changeset
   172
\<bbbV>                 code: 0x01D54D  group: letter
73461
067c23324784 clarified symbol names, notably relevant for Z_Notation;
wenzelm
parents: 73459
diff changeset
   173
\<bbbW>                 code: 0x01D54E  group: letter  group: Z_Notation
73459
1f1f4462a6ae high-quality blackboard-bold fonts from "txmia" (package "txfonts");
wenzelm
parents: 73457
diff changeset
   174
\<bbbX>                 code: 0x01D54F  group: letter
1f1f4462a6ae high-quality blackboard-bold fonts from "txmia" (package "txfonts");
wenzelm
parents: 73457
diff changeset
   175
\<bbbY>                 code: 0x01D550  group: letter
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
   176
\<int>                  code: 0x002124  group: letter
56443
ee0f7cfb7bba removed abbrev "<-" again (see c771f0fe28d1) due to conflict with important "<->" and "<-->";
wenzelm
parents: 56388
diff changeset
   177
\<leftarrow>            code: 0x002190  group: arrow  abbrev: <.
53345
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   178
\<longleftarrow>        code: 0x0027f5  group: arrow  abbrev: <.
61963
2548e7cc86fb more arrow symbols;
wenzelm
parents: 61653
diff changeset
   179
\<longlongleftarrow>    code: 0x00290e  group: arrow  abbrev: <.
2548e7cc86fb more arrow symbols;
wenzelm
parents: 61653
diff changeset
   180
\<longlonglongleftarrow> code: 0x0021e0 group: arrow  abbrev: <.
73450
c5315b89c1bf more Z_Notation symbols, as proposed by Simon Foster;
wenzelm
parents: 73447
diff changeset
   181
\<rightarrow>           code: 0x002192  group: arrow  group: Z_Notation  abbrev: .>  abbrev: ->
53345
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   182
\<longrightarrow>       code: 0x0027f6  group: arrow  abbrev: .>  abbrev: -->
61963
2548e7cc86fb more arrow symbols;
wenzelm
parents: 61653
diff changeset
   183
\<longlongrightarrow>   code: 0x00290f  group: arrow  abbrev: .>  abbrev: --->
61972
a70b89a3e02e simplified abbrevs: exploit ambiguity;
wenzelm
parents: 61964
diff changeset
   184
\<longlonglongrightarrow> code: 0x0021e2 group: arrow abbrev: .>  abbrev: --->
53345
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   185
\<Leftarrow>            code: 0x0021d0  group: arrow  abbrev: <.
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   186
\<Longleftarrow>        code: 0x0027f8  group: arrow  abbrev: <.
61964
37a0cbee00c2 more arrow symbols;
wenzelm
parents: 61963
diff changeset
   187
\<Lleftarrow>           code: 0x0021da  group: arrow  abbrev: <.
53345
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   188
\<Rightarrow>           code: 0x0021d2  group: arrow  abbrev: .>  abbrev: =>
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   189
\<Longrightarrow>       code: 0x0027f9  group: arrow  abbrev: .>  abbrev: ==>
61964
37a0cbee00c2 more arrow symbols;
wenzelm
parents: 61963
diff changeset
   190
\<Rrightarrow>          code: 0x0021db  group: arrow  abbrev: .>
73457
3ede182a479a further clarification of Z Notation symbols (notably glyphs 0x2119, 0x2A1F, 0x2982, 0x2A3E), by Simon Foster;
wenzelm
parents: 73456
diff changeset
   191
\<leftrightarrow>       code: 0x002194  group: arrow  group: Z_Notation  abbrev: <>  abbrev: <->
53345
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   192
\<longleftrightarrow>   code: 0x0027f7  group: arrow  abbrev: <>  abbrev: <->  abbrev: <-->
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   193
\<Leftrightarrow>       code: 0x0021d4  group: arrow  abbrev: <>
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   194
\<Longleftrightarrow>   code: 0x0027fa  group: arrow  abbrev: <>
73457
3ede182a479a further clarification of Z Notation symbols (notably glyphs 0x2119, 0x2A1F, 0x2982, 0x2A3E), by Simon Foster;
wenzelm
parents: 73456
diff changeset
   195
\<mapsto>               code: 0x0021a6  group: arrow  group: Z_Notation  abbrev: .>  abbrev: |->
53345
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   196
\<longmapsto>           code: 0x0027fc  group: arrow  abbrev: .>  abbrev: |-->
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   197
\<midarrow>             code: 0x002500  group: arrow  abbrev: <>
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   198
\<Midarrow>             code: 0x002550  group: arrow  abbrev: <>
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   199
\<hookleftarrow>        code: 0x0021a9  group: arrow  abbrev: <.
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   200
\<hookrightarrow>       code: 0x0021aa  group: arrow  abbrev: .>
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   201
\<leftharpoondown>      code: 0x0021bd  group: arrow  abbrev: <.
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   202
\<rightharpoondown>     code: 0x0021c1  group: arrow  abbrev: .>
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   203
\<leftharpoonup>        code: 0x0021bc  group: arrow  abbrev: <.
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   204
\<rightharpoonup>       code: 0x0021c0  group: arrow  abbrev: .>
8c333d659e8f uniform abbrevs for left/right arrows;
wenzelm
parents: 53344
diff changeset
   205
\<rightleftharpoons>    code: 0x0021cc  group: arrow  abbrev: <> abbrev: ==
73450
c5315b89c1bf more Z_Notation symbols, as proposed by Simon Foster;
wenzelm
parents: 73447
diff changeset
   206
\<leadsto>              code: 0x00219d  group: arrow  group: Z_Notation  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
   207
\<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
   208
\<downharpoonright>     code: 0x0021c2  group: arrow
73457
3ede182a479a further clarification of Z Notation symbols (notably glyphs 0x2119, 0x2A1F, 0x2982, 0x2A3E), by Simon Foster;
wenzelm
parents: 73456
diff changeset
   209
\<upharpoonleft>        code: 0x0021bf  group: arrow  group: Z_Notation
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
   210
#\<upharpoonright>       code: 0x0021be  group: arrow
73457
3ede182a479a further clarification of Z Notation symbols (notably glyphs 0x2119, 0x2A1F, 0x2982, 0x2A3E), by Simon Foster;
wenzelm
parents: 73456
diff changeset
   211
\<restriction>          code: 0x0021be  group: operator  group: Z_Notation
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
   212
\<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
   213
\<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
   214
\<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
   215
\<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
   216
\<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
   217
\<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
   218
\<Updown>               code: 0x0021d5  group: arrow
73454
a9e0fae0107d more Z_Notation symbols, as proposed by Simon Foster;
wenzelm
parents: 73452
diff changeset
   219
\<langle>               code: 0x0027e8  group: punctuation  group: Z_Notation  abbrev: <<
a9e0fae0107d more Z_Notation symbols, as proposed by Simon Foster;
wenzelm
parents: 73452
diff changeset
   220
\<rangle>               code: 0x0027e9  group: punctuation  group: Z_Notation  abbrev: >>
a9e0fae0107d more Z_Notation symbols, as proposed by Simon Foster;
wenzelm
parents: 73452
diff changeset
   221
\<llangle>              code: 0x0027ea  group: punctuation  group: Z_Notation  abbrev: <<
a9e0fae0107d more Z_Notation symbols, as proposed by Simon Foster;
wenzelm
parents: 73452
diff changeset
   222
\<rrangle>              code: 0x0027eb  group: punctuation  group: Z_Notation  abbrev: >>
53320
17b887110cc1 more symbol abbrevs;
wenzelm
parents: 53319
diff changeset
   223
\<lceil>                code: 0x002308  group: punctuation  abbrev: [.
17b887110cc1 more symbol abbrevs;
wenzelm
parents: 53319
diff changeset
   224
\<rceil>                code: 0x002309  group: punctuation  abbrev: .]
17b887110cc1 more symbol abbrevs;
wenzelm
parents: 53319
diff changeset
   225
\<lfloor>               code: 0x00230a  group: punctuation  abbrev: [.
17b887110cc1 more symbol abbrevs;
wenzelm
parents: 53319
diff changeset
   226
\<rfloor>               code: 0x00230b  group: punctuation  abbrev: .]
73454
a9e0fae0107d more Z_Notation symbols, as proposed by Simon Foster;
wenzelm
parents: 73452
diff changeset
   227
\<lparr>                code: 0x002987  group: punctuation  group: Z_Notation  abbrev: (|
a9e0fae0107d more Z_Notation symbols, as proposed by Simon Foster;
wenzelm
parents: 73452
diff changeset
   228
\<rparr>                code: 0x002988  group: punctuation  group: Z_Notation  abbrev: |)
a9e0fae0107d more Z_Notation symbols, as proposed by Simon Foster;
wenzelm
parents: 73452
diff changeset
   229
\<lbrakk>               code: 0x0027e6  group: punctuation  group: Z_Notation  abbrev: [|
a9e0fae0107d more Z_Notation symbols, as proposed by Simon Foster;
wenzelm
parents: 73452
diff changeset
   230
\<rbrakk>               code: 0x0027e7  group: punctuation  group: Z_Notation  abbrev: |]
53319
5f310fb79c62 misc tuning -- reduce conflicts;
wenzelm
parents: 53317
diff changeset
   231
\<lbrace>               code: 0x002983  group: punctuation  abbrev: {|
5f310fb79c62 misc tuning -- reduce conflicts;
wenzelm
parents: 53317
diff changeset
   232
\<rbrace>               code: 0x002984  group: punctuation  abbrev: |}
73446
d1c4c2395650 more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
wenzelm
parents: 72763
diff changeset
   233
\<lblot>                code: 0x002989  group: punctuation  group: Z_Notation  abbrev: <<
d1c4c2395650 more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
wenzelm
parents: 72763
diff changeset
   234
\<rblot>                code: 0x00298A  group: punctuation  group: Z_Notation  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
   235
\<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
   236
\<guillemotright>       code: 0x0000bb  group: punctuation  abbrev: >>
50188
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
   237
\<bottom>               code: 0x0022a5  group: logic
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
   238
\<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
   239
\<and>                  code: 0x002227  group: logic  abbrev: /\  abbrev: &
50188
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
   240
\<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
   241
\<or>                   code: 0x002228  group: logic  abbrev: \/  abbrev: |
50188
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
   242
\<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
   243
\<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
   244
\<exists>               code: 0x002203  group: logic  abbrev: ?  abbrev: EX
50188
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
   245
\<nexists>              code: 0x002204  group: logic  abbrev: ~?
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
   246
\<not>                  code: 0x0000ac  group: logic  abbrev: ~
62440
31fa592761da symbol interpretation for \<circle>;
wenzelm
parents: 62260
diff changeset
   247
\<circle>               code: 0x0025cb  group: logic
50188
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
   248
\<box>                  code: 0x0025a1  group: logic
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
   249
\<diamond>              code: 0x0025c7  group: logic
62108
0046bacc5f5b \<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents: 62025
diff changeset
   250
\<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
   251
\<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
   252
\<Turnstile>            code: 0x0022a8  group: relation  abbrev: |=
53319
5f310fb79c62 misc tuning -- reduce conflicts;
wenzelm
parents: 53317
diff changeset
   253
\<tturnstile>           code: 0x0022a9  group: relation  abbrev: |-
5f310fb79c62 misc tuning -- reduce conflicts;
wenzelm
parents: 53317
diff changeset
   254
\<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
   255
\<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
   256
\<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
   257
\<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
   258
\<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
   259
\<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
   260
\<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
   261
\<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
   262
\<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
   263
\<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
   264
\<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
   265
\<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
   266
\<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
   267
\<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
   268
\<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
   269
\<subseteq>             code: 0x002286  group: relation  abbrev: (=
53343
8dc406adbc75 added common alternative for == (its ambiguity also avoids conflict with ==>);
wenzelm
parents: 53323
diff changeset
   270
\<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
   271
\<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
   272
\<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
   273
\<sqsubseteq>           code: 0x002291  group: relation  abbrev: [=
53343
8dc406adbc75 added common alternative for == (its ambiguity also avoids conflict with ==>);
wenzelm
parents: 53323
diff changeset
   274
\<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
   275
\<inter>                code: 0x002229  group: operator  abbrev: Int
53344
9a5eaa6b0154 more abbrevs according to Isabelle/HOL ASCII replacement syntax;
wenzelm
parents: 53343
diff changeset
   276
\<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
   277
\<union>                code: 0x00222a  group: operator  abbrev: Un
53344
9a5eaa6b0154 more abbrevs according to Isabelle/HOL ASCII replacement syntax;
wenzelm
parents: 53343
diff changeset
   278
\<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
   279
\<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
   280
\<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
   281
\<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
   282
\<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
   283
\<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
   284
\<propto>               code: 0x00221d  group: operator
73454
a9e0fae0107d more Z_Notation symbols, as proposed by Simon Foster;
wenzelm
parents: 73452
diff changeset
   285
\<uplus>                code: 0x00228e  group: operator  group: Z_Notation
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
   286
\<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
   287
\<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
   288
\<sim>                  code: 0x00223c  group: relation
53319
5f310fb79c62 misc tuning -- reduce conflicts;
wenzelm
parents: 53317
diff changeset
   289
\<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
   290
\<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
   291
\<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
   292
\<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
   293
\<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
   294
\<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
   295
\<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
   296
\<frown>                code: 0x002322  group: relation
43486
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   297
\<Join>                 code: 0x0022c8
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   298
\<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
   299
\<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
   300
\<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
   301
\<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
   302
\<succeq>               code: 0x00227d  group: relation
73468
86b900eff9bf clarified group (but hard to tell);
wenzelm
parents: 73467
diff changeset
   303
\<parallel>             code: 0x002225  group: relation  abbrev: ||
74433
ec1774613824 support symbol \<Parallel>, based on \bigparallel from stdmaryd (stmary10.pfb: move y=1100, scale 222%, embolden by 40 units, adjust spacing);
wenzelm
parents: 74341
diff changeset
   304
\<Parallel>             code: 0x002016  group: relation  abbrev: ||
73468
86b900eff9bf clarified group (but hard to tell);
wenzelm
parents: 73467
diff changeset
   305
\<interleave>           code: 0x002af4  group: relation  abbrev: ||
86b900eff9bf clarified group (but hard to tell);
wenzelm
parents: 73467
diff changeset
   306
\<sslash>               code: 0x002afd  group: relation  abbrev: ||
53320
17b887110cc1 more symbol abbrevs;
wenzelm
parents: 53319
diff changeset
   307
\<bar>                  code: 0x0000a6  group: punctuation  abbrev: ||
70369
6c65447b8a64 added \<bbar>;
wenzelm
parents: 70368
diff changeset
   308
\<bbar>                 code: 0x002aff  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
   309
\<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
   310
\<minusplus>            code: 0x002213  group: operator
55786
96861130f922 more symbol abbrevs to support HOL library maintenance;
wenzelm
parents: 55546
diff changeset
   311
\<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
   312
\<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
   313
\<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
   314
\<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
   315
\<bullet>               code: 0x002219  group: operator
53323
5fa77d6ad63d single-letter abbrev does not make sense -- too many candidates;
wenzelm
parents: 53321
diff changeset
   316
\<circ>                 code: 0x002218  group: operator
43486
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   317
\<dagger>               code: 0x002020
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   318
\<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
   319
\<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
   320
\<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
   321
\<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
   322
\<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
   323
\<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
   324
\<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
   325
\<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
   326
\<triangleq>            code: 0x00225c  group: relation
73450
c5315b89c1bf more Z_Notation symbols, as proposed by Simon Foster;
wenzelm
parents: 73447
diff changeset
   327
\<oplus>                code: 0x002295  group: operator  group: Z_Notation
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
   328
\<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
   329
\<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
   330
\<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
   331
\<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
   332
\<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
   333
\<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
   334
\<oslash>               code: 0x002298  group: operator
50188
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
   335
\<dots>                 code: 0x002026  group: punctuation abbrev: ...
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
   336
\<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
   337
\<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
   338
\<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
   339
\<Coprod>               code: 0x002210  group: operator
43486
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   340
\<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
   341
\<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
   342
\<ointegral>            code: 0x00222e  group: operator
43486
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   343
\<clubsuit>             code: 0x002663
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   344
\<diamondsuit>          code: 0x002662
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   345
\<heartsuit>            code: 0x002661
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   346
\<spadesuit>            code: 0x002660
50193
3ef3e3e75166 tuned symbol groups;
wenzelm
parents: 50188
diff changeset
   347
\<aleph>                code: 0x002135
43486
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   348
\<emptyset>             code: 0x002205
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   349
\<nabla>                code: 0x002207
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   350
\<partial>              code: 0x002202
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   351
\<flat>                 code: 0x00266d
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   352
\<natural>              code: 0x00266e
73454
a9e0fae0107d more Z_Notation symbols, as proposed by Simon Foster;
wenzelm
parents: 73452
diff changeset
   353
\<sharp>                code: 0x00266f  group: Z_Notation
43486
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   354
\<angle>                code: 0x002220
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   355
\<copyright>            code: 0x0000a9
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   356
\<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
   357
\<hyphen>               code: 0x002010  group: punctuation
69361
0d84e3db67c2 clarified symbol groups;
wenzelm
parents: 69343
diff changeset
   358
\<inverse>              code: 0x0000af  group: operator
70368
b67737bc5bd1 added \<sqdot>;
wenzelm
parents: 70204
diff changeset
   359
\<sqdot>                code: 0x0000b7  group: punctuation
50188
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
   360
\<onequarter>           code: 0x0000bc  group: digit
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
   361
\<onehalf>              code: 0x0000bd  group: digit
6d22f5a7335c tuned symbol groups;
wenzelm
parents: 50159
diff changeset
   362
\<threequarters>        code: 0x0000be  group: digit
27899
a152c8a38b7d removed redundant "symbol" property;
wenzelm
parents: 27898
diff changeset
   363
\<ordfeminine>          code: 0x0000aa
a152c8a38b7d removed redundant "symbol" property;
wenzelm
parents: 27898
diff changeset
   364
\<ordmasculine>         code: 0x0000ba
a152c8a38b7d removed redundant "symbol" property;
wenzelm
parents: 27898
diff changeset
   365
\<section>              code: 0x0000a7
61592
d80eb8f6eb47 retain traditional rendering of \<paragraph>;
wenzelm
parents: 61584
diff changeset
   366
\<paragraph>            code: 0x0000b6
27899
a152c8a38b7d removed redundant "symbol" property;
wenzelm
parents: 27898
diff changeset
   367
\<exclamdown>           code: 0x0000a1
a152c8a38b7d removed redundant "symbol" property;
wenzelm
parents: 27898
diff changeset
   368
\<questiondown>         code: 0x0000bf
27900
fdd6e68e29d9 added some abbrevs;
wenzelm
parents: 27899
diff changeset
   369
\<euro>                 code: 0x0020ac
27899
a152c8a38b7d removed redundant "symbol" property;
wenzelm
parents: 27898
diff changeset
   370
\<pounds>               code: 0x0000a3
a152c8a38b7d removed redundant "symbol" property;
wenzelm
parents: 27898
diff changeset
   371
\<yen>                  code: 0x0000a5
a152c8a38b7d removed redundant "symbol" property;
wenzelm
parents: 27898
diff changeset
   372
\<cent>                 code: 0x0000a2
a152c8a38b7d removed redundant "symbol" property;
wenzelm
parents: 27898
diff changeset
   373
\<currency>             code: 0x0000a4
43486
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   374
\<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
   375
\<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
   376
\<mho>                  code: 0x002127  group: operator
43486
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   377
\<lozenge>              code: 0x0025ca
50193
3ef3e3e75166 tuned symbol groups;
wenzelm
parents: 50188
diff changeset
   378
\<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
   379
\<wrong>                code: 0x002240  group: relation
27899
a152c8a38b7d removed redundant "symbol" property;
wenzelm
parents: 27898
diff changeset
   380
\<acute>                code: 0x0000b4
43486
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   381
\<index>                code: 0x000131
27899
a152c8a38b7d removed redundant "symbol" property;
wenzelm
parents: 27898
diff changeset
   382
\<dieresis>             code: 0x0000a8
a152c8a38b7d removed redundant "symbol" property;
wenzelm
parents: 27898
diff changeset
   383
\<cedilla>              code: 0x0000b8
a152c8a38b7d removed redundant "symbol" property;
wenzelm
parents: 27898
diff changeset
   384
\<hungarumlaut>         code: 0x0002dd
69361
0d84e3db67c2 clarified symbol groups;
wenzelm
parents: 69343
diff changeset
   385
\<bind>                 code: 0x00291c  group: operator  abbrev: >>=
73450
c5315b89c1bf more Z_Notation symbols, as proposed by Simon Foster;
wenzelm
parents: 73447
diff changeset
   386
\<then>                 code: 0x002aa2  group: operator  group: Z_Notation  abbrev: >>
43486
4a1ef71fbf5f removed obsolete font specification;
wenzelm
parents: 43463
diff changeset
   387
\<some>                 code: 0x0003f5
73456
0cc9c2d43957 clarified \<Zcomp> (small) vs. \<Zsemi> (big);
wenzelm
parents: 73454
diff changeset
   388
\<Zcomp>                code: 0x002A3E  group: Z_Notation  group: punctuation
73446
d1c4c2395650 more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
wenzelm
parents: 72763
diff changeset
   389
\<Zinj>                 code: 0x0021A3  group: Z_Notation  group: arrow  abbrev: .>
d1c4c2395650 more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
wenzelm
parents: 72763
diff changeset
   390
\<Zpinj>                code: 0x002914  group: Z_Notation  group: arrow  abbrev: .>
d1c4c2395650 more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
wenzelm
parents: 72763
diff changeset
   391
\<Zfinj>                code: 0x002915  group: Z_Notation  group: arrow  abbrev: .>
d1c4c2395650 more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
wenzelm
parents: 72763
diff changeset
   392
\<Zsurj>                code: 0x0021A0  group: Z_Notation  group: arrow  abbrev: .>
d1c4c2395650 more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
wenzelm
parents: 72763
diff changeset
   393
\<Zpsurj>               code: 0x002900  group: Z_Notation  group: arrow  abbrev: .>
d1c4c2395650 more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
wenzelm
parents: 72763
diff changeset
   394
\<Zbij>                 code: 0x002916  group: Z_Notation  group: arrow  abbrev: .>
d1c4c2395650 more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
wenzelm
parents: 72763
diff changeset
   395
\<Zpfun>                code: 0x0021F8  group: Z_Notation  group: arrow  abbrev: .>
d1c4c2395650 more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
wenzelm
parents: 72763
diff changeset
   396
\<Zffun>                code: 0x0021FB  group: Z_Notation  group: arrow  abbrev: .>
d1c4c2395650 more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
wenzelm
parents: 72763
diff changeset
   397
\<Zdres>                code: 0x0025C1  group: Z_Notation  group: relation
d1c4c2395650 more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
wenzelm
parents: 72763
diff changeset
   398
\<Zndres>               code: 0x002A64  group: Z_Notation  group: relation
d1c4c2395650 more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
wenzelm
parents: 72763
diff changeset
   399
\<Zrres>                code: 0x0025B7  group: Z_Notation  group: relation
d1c4c2395650 more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
wenzelm
parents: 72763
diff changeset
   400
\<Znrres>               code: 0x002A65  group: Z_Notation  group: relation
d1c4c2395650 more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
wenzelm
parents: 72763
diff changeset
   401
\<Zspot>                code: 0x002981  group: Z_Notation  group: punctuation
73457
3ede182a479a further clarification of Z Notation symbols (notably glyphs 0x2119, 0x2A1F, 0x2982, 0x2A3E), by Simon Foster;
wenzelm
parents: 73456
diff changeset
   402
\<Zsemi>                code: 0x002A1F  group: Z_Notation
73447
2200a19cac72 prefer explicit \<Zproject> (with its own Unicode codepoint);
wenzelm
parents: 73446
diff changeset
   403
\<Zproject>             code: 0x002A21  group: Z_Notation  group: operator
73446
d1c4c2395650 more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
wenzelm
parents: 72763
diff changeset
   404
\<Ztypecolon>           code: 0x002982  group: Z_Notation  group: relation
d1c4c2395650 more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
wenzelm
parents: 72763
diff changeset
   405
\<Zhide>                code: 0x0029F9  group: Z_Notation  group: operator
d1c4c2395650 more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
wenzelm
parents: 72763
diff changeset
   406
\<Zcat>                 code: 0x002040  group: Z_Notation  group: operator
73454
a9e0fae0107d more Z_Notation symbols, as proposed by Simon Foster;
wenzelm
parents: 73452
diff changeset
   407
\<Zinbag>               code: 0x0022FF  group: Z_Notation  group: relation
73457
3ede182a479a further clarification of Z Notation symbols (notably glyphs 0x2119, 0x2A1F, 0x2982, 0x2A3E), by Simon Foster;
wenzelm
parents: 73456
diff changeset
   408
\<Zprime>               code: 0x002032  group: Z_Notation  group: punctuation
59974
b911c8ba0b69 added symbol for \<hole> (from DejaVuSansMono and DejaVuSansMono-Bold version 2.34);
wenzelm
parents: 57081
diff changeset
   409
\<hole>                 code: 0x002311
55015
e33c5bd729ff added \<newline> symbol, which is used for char/string literals in HOL;
wenzelm
parents: 53345
diff changeset
   410
\<newline>              code: 0x0023ce
69343
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   411
\<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
   412
\<^cancel>              code: 0x002326  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
67430
149b742070e9 support for completion;
wenzelm
parents: 67424
diff changeset
   413
\<^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
   414
\<^marker>              code: 0x002710  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
73467
090add96f5f9 more glyphs proposed by Simon Foster: 0x002713, 0x002717, 0x002af4, 0x002afb, 0x002afd;
wenzelm
parents: 73461
diff changeset
   415
\<checkmark>            code: 0x002713
090add96f5f9 more glyphs proposed by Simon Foster: 0x002713, 0x002717, 0x002af4, 0x002afb, 0x002afd;
wenzelm
parents: 73461
diff changeset
   416
\<crossmark>            code: 0x002717
69343
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 67470
diff changeset
   417
\<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
   418
\<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
   419
\<^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
   420
\<^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
   421
\<^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
   422
\<^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
   423
\<^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
   424
\<^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
   425
\<^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
   426
\<^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
   427
\<^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
   428
\<^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
   429
\<^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
   430
\<^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
   431
\<^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
   432
\<^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
   433
\<^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
   434
\<^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
   435
\<^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
   436
\<^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
   437
\<^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
   438
\<^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
   439
\<^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
   440
\<^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
   441
\<^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
   442
\<^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
   443
\<^action>              code: 0x00261b  group: icon  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
67311
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   444
\<^assert>
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   445
\<^binding>             argument: cartouche
73550
2f6855142a8c support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents: 73468
diff changeset
   446
\<^can>                 argument: cartouche
67311
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   447
\<^class>               argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   448
\<^class_syntax>        argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   449
\<^command_keyword>     argument: cartouche
70204
230188a56a9e completion for \<^const>, although it often requires an extra argument;
wenzelm
parents: 70015
diff changeset
   450
\<^const>               argument: cartouche
67311
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   451
\<^const_abbrev>        argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   452
\<^const_name>          argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   453
\<^const_syntax>        argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   454
\<^context>
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   455
\<^cprop>               argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   456
\<^cterm>               argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   457
\<^ctyp>                argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   458
\<^keyword>             argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   459
\<^locale>              argument: cartouche
74341
edf8b141a8c4 ML antiquotations for object-logic judgment;
wenzelm
parents: 74318
diff changeset
   460
\<^make_judgment>
edf8b141a8c4 ML antiquotations for object-logic judgment;
wenzelm
parents: 74318
diff changeset
   461
\<^dest_judgment>
67311
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   462
\<^make_string>
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   463
\<^method>              argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   464
\<^named_theorems>      argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   465
\<^nonterminal>         argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   466
\<^path>                argument: cartouche
70015
c8e08d8ffb93 clarified signature: more explicit type Path.binding;
wenzelm
parents: 69891
diff changeset
   467
\<^path_binding>        argument: cartouche
67311
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   468
\<^plugin>              argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   469
\<^print>
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   470
\<^prop>                argument: cartouche
71902
1529336eaedc check bash functions against Isabelle settings environment;
wenzelm
parents: 71887
diff changeset
   471
\<^bash_function>       argument: cartouche
71881
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 70565
diff changeset
   472
\<^scala>               argument: cartouche
71de0a253842 proper check of registered Scala functions;
wenzelm
parents: 70565
diff changeset
   473
\<^scala_function>      argument: cartouche
71887
f7d15620dd8e antiquotations for Scala entities;
wenzelm
parents: 71881
diff changeset
   474
\<^scala_method>        argument: cartouche
f7d15620dd8e antiquotations for Scala entities;
wenzelm
parents: 71881
diff changeset
   475
\<^scala_object>        argument: cartouche
72332
319dd5c618a5 allow Scala function execution on separate thread: better reactivity, but potential overloading of the JVM;
wenzelm
parents: 71902
diff changeset
   476
\<^scala_thread>        argument: cartouche
71887
f7d15620dd8e antiquotations for Scala entities;
wenzelm
parents: 71881
diff changeset
   477
\<^scala_type>          argument: cartouche
67470
d36fcde7e2c0 support for completion;
wenzelm
parents: 67430
diff changeset
   478
\<^session>             argument: cartouche
67311
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   479
\<^simproc>             argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   480
\<^sort>                argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   481
\<^syntax_const>        argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   482
\<^system_option>       argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   483
\<^term>                argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   484
\<^theory>              argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   485
\<^theory_context>      argument: cartouche
72763
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72332
diff changeset
   486
\<^tool>                argument: cartouche
73550
2f6855142a8c support for ML special forms: modified evaluation similar to Scheme;
wenzelm
parents: 73468
diff changeset
   487
\<^try>                 argument: cartouche
74290
b2ad24b5a42c more antiquotations;
wenzelm
parents: 73586
diff changeset
   488
\<^tvar>                argument: cartouche
67311
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   489
\<^typ>                 argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   490
\<^type_abbrev>         argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   491
\<^type_name>           argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   492
\<^type_syntax>         argument: cartouche
74290
b2ad24b5a42c more antiquotations;
wenzelm
parents: 73586
diff changeset
   493
\<^var>                 argument: cartouche
70565
d0b75c59beca added ML antiquotation @{oracle_name};
wenzelm
parents: 70371
diff changeset
   494
\<^oracle_name>         argument: cartouche
74291
b83fa8f3a271 ML antiquotations for type constructors and term constants;
wenzelm
parents: 74290
diff changeset
   495
\<^Const>               argument: cartouche
b83fa8f3a271 ML antiquotations for type constructors and term constants;
wenzelm
parents: 74290
diff changeset
   496
\<^Const_>              argument: cartouche
74318
3360ea6b659d more control symbols;
wenzelm
parents: 74291
diff changeset
   497
\<^Const_fn>            argument: cartouche
74291
b83fa8f3a271 ML antiquotations for type constructors and term constants;
wenzelm
parents: 74290
diff changeset
   498
\<^Type>                argument: cartouche
74318
3360ea6b659d more control symbols;
wenzelm
parents: 74291
diff changeset
   499
\<^Type_fn>             argument: cartouche
67311
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   500
\<^code>                argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   501
\<^computation>         argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   502
\<^computation_conv>    argument: cartouche
3869b2400e22 more completion templates;
wenzelm
parents: 67305
diff changeset
   503
\<^computation_check>   argument: cartouche
73586
76d0b6597c91 support for conditional ML text;
wenzelm
parents: 73550
diff changeset
   504
\<^if_linux>            argument: cartouche
76d0b6597c91 support for conditional ML text;
wenzelm
parents: 73550
diff changeset
   505
\<^if_macos>            argument: cartouche
76d0b6597c91 support for conditional ML text;
wenzelm
parents: 73550
diff changeset
   506
\<^if_windows>          argument: cartouche
76d0b6597c91 support for conditional ML text;
wenzelm
parents: 73550
diff changeset
   507
\<^if_unix>             argument: cartouche
76d0b6597c91 support for conditional ML text;
wenzelm
parents: 73550
diff changeset
   508