author | wenzelm |
Sat, 16 Oct 2021 20:21:13 +0200 | |
changeset 74532 | 64d1b02327a4 |
parent 74433 | ec1774613824 |
child 74568 | 7f311d474cf9 |
permissions | -rw-r--r-- |
27898 | 1 |
# Default interpretation of some Isabelle symbols |
2 |
||
50188 | 3 |
\<zero> code: 0x01d7ec group: digit |
4 |
\<one> code: 0x01d7ed group: digit |
|
5 |
\<two> code: 0x01d7ee group: digit |
|
6 |
\<three> code: 0x01d7ef group: digit |
|
7 |
\<four> code: 0x01d7f0 group: digit |
|
8 |
\<five> code: 0x01d7f1 group: digit |
|
9 |
\<six> code: 0x01d7f2 group: digit |
|
10 |
\<seven> code: 0x01d7f3 group: digit |
|
11 |
\<eight> code: 0x01d7f4 group: digit |
|
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 | 178 |
\<longleftarrow> code: 0x0027f5 group: arrow abbrev: <. |
61963 | 179 |
\<longlongleftarrow> code: 0x00290e group: arrow abbrev: <. |
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 | 182 |
\<longrightarrow> code: 0x0027f6 group: arrow abbrev: .> abbrev: --> |
61963 | 183 |
\<longlongrightarrow> code: 0x00290f group: arrow abbrev: .> abbrev: ---> |
61972 | 184 |
\<longlonglongrightarrow> code: 0x0021e2 group: arrow abbrev: .> abbrev: ---> |
53345 | 185 |
\<Leftarrow> code: 0x0021d0 group: arrow abbrev: <. |
186 |
\<Longleftarrow> code: 0x0027f8 group: arrow abbrev: <. |
|
61964 | 187 |
\<Lleftarrow> code: 0x0021da group: arrow abbrev: <. |
53345 | 188 |
\<Rightarrow> code: 0x0021d2 group: arrow abbrev: .> abbrev: => |
189 |
\<Longrightarrow> code: 0x0027f9 group: arrow abbrev: .> abbrev: ==> |
|
61964 | 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 | 192 |
\<longleftrightarrow> code: 0x0027f7 group: arrow abbrev: <> abbrev: <-> abbrev: <--> |
193 |
\<Leftrightarrow> code: 0x0021d4 group: arrow abbrev: <> |
|
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 | 196 |
\<longmapsto> code: 0x0027fc group: arrow abbrev: .> abbrev: |--> |
197 |
\<midarrow> code: 0x002500 group: arrow abbrev: <> |
|
198 |
\<Midarrow> code: 0x002550 group: arrow abbrev: <> |
|
199 |
\<hookleftarrow> code: 0x0021a9 group: arrow abbrev: <. |
|
200 |
\<hookrightarrow> code: 0x0021aa group: arrow abbrev: .> |
|
201 |
\<leftharpoondown> code: 0x0021bd group: arrow abbrev: <. |
|
202 |
\<rightharpoondown> code: 0x0021c1 group: arrow abbrev: .> |
|
203 |
\<leftharpoonup> code: 0x0021bc group: arrow abbrev: <. |
|
204 |
\<rightharpoonup> code: 0x0021c0 group: arrow abbrev: .> |
|
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 | 223 |
\<lceil> code: 0x002308 group: punctuation abbrev: [. |
224 |
\<rceil> code: 0x002309 group: punctuation abbrev: .] |
|
225 |
\<lfloor> code: 0x00230a group: punctuation abbrev: [. |
|
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 | 231 |
\<lbrace> code: 0x002983 group: punctuation abbrev: {| |
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 | 237 |
\<bottom> code: 0x0022a5 group: logic |
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 | 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 | 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 | 245 |
\<nexists> code: 0x002204 group: logic abbrev: ~? |
246 |
\<not> code: 0x0000ac group: logic abbrev: ~ |
|
62440 | 247 |
\<circle> code: 0x0025cb group: logic |
50188 | 248 |
\<box> code: 0x0025a1 group: logic |
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 | 253 |
\<tturnstile> code: 0x0022a9 group: relation abbrev: |- |
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 | 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 | 297 |
\<Join> code: 0x0022c8 |
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 | 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 | 305 |
\<interleave> code: 0x002af4 group: relation abbrev: || |
306 |
\<sslash> code: 0x002afd group: relation abbrev: || |
|
53320 | 307 |
\<bar> code: 0x0000a6 group: punctuation abbrev: || |
70369 | 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 | 317 |
\<dagger> code: 0x002020 |
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 | 335 |
\<dots> code: 0x002026 group: punctuation abbrev: ... |
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 | 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 | 343 |
\<clubsuit> code: 0x002663 |
344 |
\<diamondsuit> code: 0x002662 |
|
345 |
\<heartsuit> code: 0x002661 |
|
346 |
\<spadesuit> code: 0x002660 |
|
50193 | 347 |
\<aleph> code: 0x002135 |
43486 | 348 |
\<emptyset> code: 0x002205 |
349 |
\<nabla> code: 0x002207 |
|
350 |
\<partial> code: 0x002202 |
|
351 |
\<flat> code: 0x00266d |
|
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 | 354 |
\<angle> code: 0x002220 |
355 |
\<copyright> code: 0x0000a9 |
|
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 | 358 |
\<inverse> code: 0x0000af group: operator |
70368 | 359 |
\<sqdot> code: 0x0000b7 group: punctuation |
50188 | 360 |
\<onequarter> code: 0x0000bc group: digit |
361 |
\<onehalf> code: 0x0000bd group: digit |
|
362 |
\<threequarters> code: 0x0000be group: digit |
|
27899 | 363 |
\<ordfeminine> code: 0x0000aa |
364 |
\<ordmasculine> code: 0x0000ba |
|
365 |
\<section> code: 0x0000a7 |
|
61592 | 366 |
\<paragraph> code: 0x0000b6 |
27899 | 367 |
\<exclamdown> code: 0x0000a1 |
368 |
\<questiondown> code: 0x0000bf |
|
27900 | 369 |
\<euro> code: 0x0020ac |
27899 | 370 |
\<pounds> code: 0x0000a3 |
371 |
\<yen> code: 0x0000a5 |
|
372 |
\<cent> code: 0x0000a2 |
|
373 |
\<currency> code: 0x0000a4 |
|
43486 | 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 | 377 |
\<lozenge> code: 0x0025ca |
50193 | 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 | 380 |
\<acute> code: 0x0000b4 |
43486 | 381 |
\<index> code: 0x000131 |
27899 | 382 |
\<dieresis> code: 0x0000a8 |
383 |
\<cedilla> code: 0x0000b8 |
|
384 |
\<hungarumlaut> code: 0x0002dd |
|
69361 | 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 | 387 |
\<some> code: 0x0003f5 |
73456 | 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 | 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 | 444 |
\<^assert> |
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 | 447 |
\<^class> argument: cartouche |
448 |
\<^class_syntax> argument: cartouche |
|
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 | 451 |
\<^const_abbrev> argument: cartouche |
452 |
\<^const_name> argument: cartouche |
|
453 |
\<^const_syntax> argument: cartouche |
|
454 |
\<^context> |
|
455 |
\<^cprop> argument: cartouche |
|
456 |
\<^cterm> argument: cartouche |
|
457 |
\<^ctyp> argument: cartouche |
|
458 |
\<^keyword> argument: cartouche |
|
459 |
\<^locale> argument: cartouche |
|
74341 | 460 |
\<^make_judgment> |
461 |
\<^dest_judgment> |
|
67311 | 462 |
\<^make_string> |
463 |
\<^method> argument: cartouche |
|
464 |
\<^named_theorems> argument: cartouche |
|
465 |
\<^nonterminal> argument: cartouche |
|
466 |
\<^path> argument: cartouche |
|
70015
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
69891
diff
changeset
|
467 |
\<^path_binding> argument: cartouche |
67311 | 468 |
\<^plugin> argument: cartouche |
469 |
\<^print> |
|
470 |
\<^prop> argument: cartouche |
|
71902
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
71887
diff
changeset
|
471 |
\<^bash_function> argument: cartouche |
71881 | 472 |
\<^scala> argument: cartouche |
473 |
\<^scala_function> argument: cartouche |
|
71887 | 474 |
\<^scala_method> argument: cartouche |
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 | 477 |
\<^scala_type> argument: cartouche |
67470 | 478 |
\<^session> argument: cartouche |
67311 | 479 |
\<^simproc> argument: cartouche |
480 |
\<^sort> argument: cartouche |
|
481 |
\<^syntax_const> argument: cartouche |
|
482 |
\<^system_option> argument: cartouche |
|
483 |
\<^term> argument: cartouche |
|
484 |
\<^theory> argument: cartouche |
|
485 |
\<^theory_context> argument: cartouche |
|
72763 | 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 | 488 |
\<^tvar> argument: cartouche |
67311 | 489 |
\<^typ> argument: cartouche |
490 |
\<^type_abbrev> argument: cartouche |
|
491 |
\<^type_name> argument: cartouche |
|
492 |
\<^type_syntax> argument: cartouche |
|
74290 | 493 |
\<^var> argument: cartouche |
70565 | 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 | 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 | 499 |
\<^Type_fn> argument: cartouche |
67311 | 500 |
\<^code> argument: cartouche |
501 |
\<^computation> argument: cartouche |
|
502 |
\<^computation_conv> argument: cartouche |
|
503 |
\<^computation_check> argument: cartouche |
|
73586 | 504 |
\<^if_linux> argument: cartouche |
505 |
\<^if_macos> argument: cartouche |
|
506 |
\<^if_windows> argument: cartouche |
|
507 |
\<^if_unix> argument: cartouche |
|
508 |