Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Admin/xsymbol/xsymb1_12.bdf
author paulson
Tue, 23 Sep 2003 15:41:33 +0200
changeset 14200 d8598e24f8fa
parent 10048 eb9983e554fd
permissions -rw-r--r--
Removal of the Key_supply axiom (affects many possbility proofs) and minor changes

STARTFONT 2.1
COMMENT xsymb1_12.bdf --- additional font for package x-symbol
COMMENT
COMMENT Copyright (C) 1997-1999 Free Software Foundation, Inc.
COMMENT
COMMENT Author: Christoph Wedler <wedler@fmi.uni-passau.de>
COMMENT Version: $Id$
COMMENT Keywords: fonts, WYSIWYG, LaTeX, HTML, wp, math
COMMENT X-URL: http://www.fmi.uni-passau.de/~wedler/x-symbol/
COMMENT
COMMENT This font is free software; you can redistribute it and/or modify
COMMENT it under the terms of the GNU General Public License as published by
COMMENT the Free Software Foundation; either version 2, or (at your option)
COMMENT any later version.
COMMENT
COMMENT This program is distributed in the hope that it will be useful,
COMMENT but WITHOUT ANY WARRANTY; without even the implied warranty of
COMMENT MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
COMMENT GNU General Public License for more details.
COMMENT
COMMENT You should have received a copy of the GNU General Public License
COMMENT along with this program; if not, write to the Free Software
COMMENT Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
COMMENT 
COMMENT 
FONT -XSYMB-XSymb1-Medium-R-Normal--12-120-75-75-P-74-XSYMB-XSymb1
SIZE 12 75 75
FONTBOUNDINGBOX 17 14 2 -3
STARTPROPERTIES 23
FONTNAME_REGISTRY ""
FAMILY_NAME "XSymb1"
FOUNDRY "XSYMB"
WEIGHT_NAME "Medium"
SETWIDTH_NAME "Normal"
SLANT "R"
ADD_STYLE_NAME ""
PIXEL_SIZE 12
POINT_SIZE 120
RESOLUTION_X 75
RESOLUTION_Y 75
SPACING "P"
AVERAGE_WIDTH 74
CHARSET_REGISTRY "XSYMB"
CHARSET_ENCODING "XSymb1"
CHARSET_COLLECTIONS "XSymb1"
FONT_DESCENT 3
FONT_ASCENT 11
CAP_HEIGHT 9
X_HEIGHT 6
FACE_NAME "XSymb1"
DEVICE_FONT_NAME "XSymb1"
COPYRIGHT "1997-1999 Free Software Foundation, Inc."
ENDPROPERTIES
CHARS 169
STARTCHAR verticaldots
ENCODING 33
SWIDTH 250 0
DWIDTH 5 0
BBX 1 10 2 -1
BITMAP
80
80
00
00
80
80
00
00
80
80
ENDCHAR
STARTCHAR backslash1
ENCODING 34
SWIDTH 250 0
DWIDTH 6 0
BBX 5 11 0 -2
BITMAP
80
c0
40
60
20
30
10
18
08
00
78
ENDCHAR
STARTCHAR dagger
ENCODING 35
SWIDTH 250 0
DWIDTH 7 0
BBX 5 11 1 -2
BITMAP
70
70
20
f8
20
70
70
70
70
20
20
ENDCHAR
STARTCHAR percent2
ENCODING 38
SWIDTH 833 0
DWIDTH 10 0
BBX 9 9 0 0
BITMAP
7900
9700
9200
6400
0800
1300
1480
2480
6300
ENDCHAR
STARTCHAR guilsinglright
ENCODING 39
SWIDTH 250 0
DWIDTH 5 0
BBX 3 5 1 1
BITMAP
80
40
20
40
80
ENDCHAR
STARTCHAR NG
ENCODING 40
SWIDTH 250 0
DWIDTH 9 0
BBX 7 9 1 0
BITMAP
b8
c4
82
82
82
82
82
92
9c
ENDCHAR
STARTCHAR OE
ENCODING 41
SWIDTH 1000 0
DWIDTH 12 0
BBX 10 9 1 0
BITMAP
3fc0
4400
8400
8400
87c0
8400
8400
4400
3fc0
ENDCHAR
STARTCHAR dotlessj
ENCODING 42
SWIDTH 250 0
DWIDTH 5 0
BBX 4 10 0 -3
BITMAP
10
10
10
10
10
10
10
10
10
e0
ENDCHAR
STARTCHAR ng
ENCODING 43
SWIDTH 250 0
DWIDTH 7 0
BBX 5 11 1 -3
BITMAP
00
b0
c8
88
88
88
88
88
08
28
30
ENDCHAR
STARTCHAR oe
ENCODING 44
SWIDTH 944 0
DWIDTH 11 0
BBX 9 7 1 0
BITMAP
7700
8880
8880
8f80
8800
8880
7700
ENDCHAR
STARTCHAR sharp
ENCODING 45
SWIDTH 250 0
DWIDTH 7 0
BBX 5 10 1 -1
BITMAP
10
58
78
f0
d0
58
78
f0
d0
40
ENDCHAR
STARTCHAR ceilingleft
ENCODING 46
SWIDTH 480 0
DWIDTH 6 0
BBX 4 11 1 -2
BITMAP
f0
f0
80
80
80
80
80
80
80
80
80
ENDCHAR
STARTCHAR ceilingright
ENCODING 47
SWIDTH 480 0
DWIDTH 6 0
BBX 4 11 1 -2
BITMAP
f0
f0
10
10
10
10
10
10
10
10
10
ENDCHAR
STARTCHAR zero
ENCODING 48
SWIDTH 500 0
DWIDTH 6 0
BBX 5 9 0 0
BITMAP
70
88
88
88
88
88
88
88
70
ENDCHAR
STARTCHAR one
ENCODING 49
SWIDTH 500 0
DWIDTH 6 0
BBX 3 9 1 0
BITMAP
40
c0
40
40
40
40
40
40
e0
ENDCHAR
STARTCHAR two
ENCODING 50
SWIDTH 500 0
DWIDTH 6 0
BBX 5 9 0 0
BITMAP
70
88
88
08
10
20
40
88
f8
ENDCHAR
STARTCHAR three
ENCODING 51
SWIDTH 500 0
DWIDTH 6 0
BBX 5 9 0 0
BITMAP
70
88
88
08
30
08
08
88
70
ENDCHAR
STARTCHAR four
ENCODING 52
SWIDTH 500 0
DWIDTH 6 0
BBX 6 9 0 0
BITMAP
18
28
28
48
48
88
fc
08
08
ENDCHAR
STARTCHAR five
ENCODING 53
SWIDTH 500 0
DWIDTH 6 0
BBX 5 9 0 0
BITMAP
78
40
80
f0
18
08
08
88
f0
ENDCHAR
STARTCHAR six
ENCODING 54
SWIDTH 500 0
DWIDTH 6 0
BBX 5 9 0 0
BITMAP
38
40
80
b0
c8
88
88
88
70
ENDCHAR
STARTCHAR seven
ENCODING 55
SWIDTH 500 0
DWIDTH 6 0
BBX 5 9 0 0
BITMAP
f8
88
10
10
20
20
40
40
40
ENDCHAR
STARTCHAR eight
ENCODING 56
SWIDTH 500 0
DWIDTH 6 0
BBX 5 9 0 0
BITMAP
70
88
88
c8
70
98
88
88
70
ENDCHAR
STARTCHAR nine
ENCODING 57
SWIDTH 500 0
DWIDTH 6 0
BBX 5 9 0 0
BITMAP
70
88
88
88
78
10
10
20
40
ENDCHAR
STARTCHAR star
ENCODING 58
SWIDTH 250 0
DWIDTH 7 0
BBX 5 9 1 1
BITMAP
00
00
00
00
20
a8
f8
70
d8
ENDCHAR
STARTCHAR lozenge1
ENCODING 59
SWIDTH 250 0
DWIDTH 9 0
BBX 9 9 0 -1
BITMAP
0800
1c00
3600
6300
c180
6300
3600
1c00
0800
ENDCHAR
STARTCHAR braceleft2
ENCODING 60
SWIDTH 480 0
DWIDTH 8 0
BBX 6 11 1 -2
BITMAP
1c
30
30
30
64
cc
64
30
30
30
1c
ENDCHAR
STARTCHAR circleslash
ENCODING 61
SWIDTH 768 0
DWIDTH 9 0
BBX 7 7 1 0
BITMAP
38
44
8a
92
a2
44
38
ENDCHAR
STARTCHAR braceright2
ENCODING 62
SWIDTH 480 0
DWIDTH 8 0
BBX 6 11 1 -2
BITMAP
e0
30
30
30
98
cc
98
30
30
30
e0
ENDCHAR
STARTCHAR triangle1
ENCODING 63
SWIDTH 713 0
DWIDTH 8 0
BBX 6 6 1 1
BITMAP
30
48
48
84
84
fc
ENDCHAR
STARTCHAR smalltriangleright
ENCODING 64
SWIDTH 713 0
DWIDTH 8 0
BBX 6 6 1 1
BITMAP
e0
98
84
84
98
e0
ENDCHAR
STARTCHAR triangleleft
ENCODING 65
SWIDTH 713 0
DWIDTH 10 0
BBX 8 7 1 0
BITMAP
07
1d
71
c1
71
1d
07
ENDCHAR
STARTCHAR triangle
ENCODING 66
SWIDTH 713 0
DWIDTH 9 0
BBX 7 9 1 0
BITMAP
10
10
38
28
6c
44
c6
82
fe
ENDCHAR
STARTCHAR triangleright
ENCODING 67
SWIDTH 713 0
DWIDTH 10 0
BBX 8 7 1 1
BITMAP
e0
b8
8e
83
8e
b8
e0
ENDCHAR
STARTCHAR trianglelefteq
ENCODING 68
SWIDTH 713 0
DWIDTH 11 0
BBX 8 9 1 -1
BITMAP
07
1d
71
c1
71
1d
07
00
7f
ENDCHAR
STARTCHAR trianglerighteq
ENCODING 69
SWIDTH 713 0
DWIDTH 10 0
BBX 8 9 1 -1
BITMAP
e0
b8
8e
83
8e
b8
e0
00
fe
ENDCHAR
STARTCHAR dotpunct
ENCODING 70
SWIDTH 250 0
DWIDTH 6 0
BBX 4 7 1 -2
BITMAP
40
40
00
00
00
00
f0
ENDCHAR
STARTCHAR dotequal
ENCODING 71
SWIDTH 549 0
DWIDTH 9 0
BBX 7 6 1 1
BITMAP
10
10
00
fe
00
fe
ENDCHAR
STARTCHAR wrong
ENCODING 72
SWIDTH 250 0
DWIDTH 5 0
BBX 3 10 1 0
BITMAP
00
00
c0
20
20
40
40
80
80
60
ENDCHAR
STARTCHAR natural
ENCODING 73
SWIDTH 250 0
DWIDTH 6 0
BBX 4 11 1 -2
BITMAP
80
80
b0
f0
d0
90
b0
f0
d0
10
10
ENDCHAR
STARTCHAR flat
ENCODING 74
SWIDTH 250 0
DWIDTH 6 0
BBX 4 9 1 0
BITMAP
80
80
80
f0
90
b0
b0
e0
c0
ENDCHAR
STARTCHAR epsilon1
ENCODING 75
SWIDTH 439 0
DWIDTH 6 0
BBX 5 6 1 0
BITMAP
70
88
60
80
c8
70
ENDCHAR
STARTCHAR hbar
ENCODING 76
SWIDTH 250 0
DWIDTH 7 0
BBX 6 10 0 0
BITMAP
00
40
f8
40
58
64
44
44
44
44
ENDCHAR
STARTCHAR imath
ENCODING 77
SWIDTH 329 0
DWIDTH 5 0
BBX 4 6 0 0
BITMAP
70
b0
30
60
60
70
ENDCHAR
STARTCHAR kappa1
ENCODING 78
SWIDTH 329 0
DWIDTH 8 0
BBX 6 6 1 0
BITMAP
e4
ac
38
70
d4
9c
ENDCHAR
STARTCHAR jmath
ENCODING 79
SWIDTH 329 0
DWIDTH 6 0
BBX 5 9 0 -3
BITMAP
38
58
18
18
10
30
b0
f0
60
ENDCHAR
STARTCHAR ell
ENCODING 80
SWIDTH 250 0
DWIDTH 6 0
BBX 5 11 0 0
BITMAP
00
00
30
48
48
48
48
50
e0
48
30
ENDCHAR
STARTCHAR amalg
ENCODING 81
SWIDTH 768 0
DWIDTH 9 0
BBX 8 9 0 0
BITMAP
e7
42
42
42
42
42
42
42
ff
ENDCHAR
STARTCHAR rho1
ENCODING 82
SWIDTH 549 0
DWIDTH 7 0
BBX 5 9 1 -3
BITMAP
70
88
88
88
c8
b0
80
80
70
ENDCHAR
STARTCHAR top
ENCODING 83
SWIDTH 658 0
DWIDTH 8 0
BBX 7 8 0 -1
BITMAP
fe
10
10
10
10
10
10
10
ENDCHAR
STARTCHAR Mho
ENCODING 84
SWIDTH 768 0
DWIDTH 11 0
BBX 10 9 0 0
BITMAP
f3c0
9240
2100
4080
4080
4080
2100
3300
1e00
ENDCHAR
STARTCHAR floorleft
ENCODING 85
SWIDTH 480 0
DWIDTH 7 0
BBX 5 11 1 -2
BITMAP
80
80
80
80
80
80
80
80
80
f8
f8
ENDCHAR
STARTCHAR floorright
ENCODING 86
SWIDTH 480 0
DWIDTH 7 0
BBX 5 11 1 -2
BITMAP
08
08
08
08
08
08
08
08
08
f8
f8
ENDCHAR
STARTCHAR perpendicular1
ENCODING 87
SWIDTH 658 0
DWIDTH 7 0
BBX 5 6 1 1
BITMAP
20
20
20
20
20
f8
ENDCHAR
STARTCHAR box
ENCODING 88
SWIDTH 250 0
DWIDTH 9 0
BBX 7 8 1 0
BITMAP
fe
82
82
82
82
82
82
fe
ENDCHAR
STARTCHAR asciicircum1
ENCODING 89
SWIDTH 200 0
DWIDTH 7 0
BBX 5 11 1 -2
BITMAP
20
70
d8
88
00
00
00
00
00
00
70
ENDCHAR
STARTCHAR asciitilde1
ENCODING 90
SWIDTH 200 0
DWIDTH 8 0
BBX 6 11 1 -2
BITMAP
64
b4
98
00
00
00
00
00
00
00
78
ENDCHAR
STARTCHAR leadsto
ENCODING 91
SWIDTH 987 0
DWIDTH 13 0
BBX 11 5 1 1
BITMAP
0080
4240
e7e0
1840
0080
ENDCHAR
STARTCHAR quotedbl1
ENCODING 92
SWIDTH 355 0
DWIDTH 5 0
BBX 3 3 1 6
BITMAP
a0
a0
a0
ENDCHAR
STARTCHAR longarrowleft
ENCODING 93
SWIDTH 987 0
DWIDTH 19 0
BBX 17 5 1 1
BITMAP
200000
400000
ffff80
400000
200000
ENDCHAR
STARTCHAR arrowupdown
ENCODING 94
SWIDTH 603 0
DWIDTH 7 0
BBX 5 12 1 -2
BITMAP
20
70
a8
20
20
20
20
20
20
a8
70
20
ENDCHAR
STARTCHAR longarrowright
ENCODING 95
SWIDTH 987 0
DWIDTH 19 0
BBX 17 5 1 1
BITMAP
000200
000100
ffff80
000100
000200
ENDCHAR
STARTCHAR longmapsto
ENCODING 96
SWIDTH 987 0
DWIDTH 19 0
BBX 17 5 1 1
BITMAP
800200
800100
ffff80
800100
800200
ENDCHAR
STARTCHAR longarrowdblboth
ENCODING 97
SWIDTH 987 0
DWIDTH 19 0
BBX 17 5 1 1
BITMAP
200200
7fff00
c00180
7fff00
200200
ENDCHAR
STARTCHAR longarrowdblleft
ENCODING 98
SWIDTH 987 0
DWIDTH 19 0
BBX 17 5 1 1
BITMAP
200000
7fff80
c00000
7fff80
200000
ENDCHAR
STARTCHAR arrowdblupdown
ENCODING 99
SWIDTH 603 0
DWIDTH 7 0
BBX 5 12 1 -2
BITMAP
20
70
d8
50
50
50
50
50
50
d8
70
20
ENDCHAR
STARTCHAR longarrowdblright
ENCODING 100
SWIDTH 987 0
DWIDTH 19 0
BBX 17 5 1 1
BITMAP
000200
ffff00
000180
ffff00
000200
ENDCHAR
STARTCHAR mapsto
ENCODING 101
SWIDTH 987 0
DWIDTH 13 0
BBX 11 5 1 1
BITMAP
8080
8040
ffe0
8040
8080
ENDCHAR
STARTCHAR iff
ENCODING 102
SWIDTH 987 0
DWIDTH 21 0
BBX 17 7 2 1
BITMAP
05b000
012000
25b200
752700
c00180
7fff00
200200
ENDCHAR
STARTCHAR hookleftarrow
ENCODING 103
SWIDTH 494 0
DWIDTH 13 0
BBX 11 5 1 1
BITMAP
2040
4020
ffe0
4000
2000
ENDCHAR
STARTCHAR hookrightarrow
ENCODING 104
SWIDTH 494 0
DWIDTH 13 0
BBX 11 5 1 1
BITMAP
4080
8040
7fe0
0040
0080
ENDCHAR
STARTCHAR arrownortheast
ENCODING 105
SWIDTH 494 0
DWIDTH 13 0
BBX 11 11 1 -2
BITMAP
01e0
0060
00a0
0120
0200
0400
0800
1000
2000
4000
8000
ENDCHAR
STARTCHAR arrowsoutheast
ENCODING 106
SWIDTH 494 0
DWIDTH 13 0
BBX 11 11 1 -2
BITMAP
8000
4000
2000
1000
0800
0400
0200
0120
00a0
0060
01e0
ENDCHAR
STARTCHAR arrownorthwest
ENCODING 107
SWIDTH 494 0
DWIDTH 13 0
BBX 11 11 1 -2
BITMAP
f000
c000
a000
9000
0800
0400
0200
0100
0080
0040
0020
ENDCHAR
STARTCHAR arrowsouthwest
ENCODING 108
SWIDTH 494 0
DWIDTH 13 0
BBX 11 11 1 -2
BITMAP
0020
0040
0080
0100
0200
0400
0800
9000
a000
c000
f000
ENDCHAR
STARTCHAR rightleftharpoons
ENCODING 109
SWIDTH 494 0
DWIDTH 13 0
BBX 11 7 1 0
BITMAP
0080
0040
ffe0
0000
ffe0
4000
2000
ENDCHAR
STARTCHAR leftharpoondown
ENCODING 110
SWIDTH 494 0
DWIDTH 13 0
BBX 11 3 1 1
BITMAP
ffe0
4000
2000
ENDCHAR
STARTCHAR rightharpoondown
ENCODING 111
SWIDTH 494 0
DWIDTH 13 0
BBX 11 3 1 1
BITMAP
ffe0
0040
0080
ENDCHAR
STARTCHAR leftharpoonup
ENCODING 112
SWIDTH 494 0
DWIDTH 13 0
BBX 11 3 1 2
BITMAP
2000
4000
ffe0
ENDCHAR
STARTCHAR rightharpoonup
ENCODING 113
SWIDTH 494 0
DWIDTH 13 0
BBX 11 3 1 3
BITMAP
0080
0040
ffe0
ENDCHAR
STARTCHAR bardbl
ENCODING 114
SWIDTH 480 0
DWIDTH 6 0
BBX 4 11 1 -2
BITMAP
90
90
90
90
90
90
90
90
90
90
90
ENDCHAR
STARTCHAR shortbardbl
ENCODING 115
SWIDTH 480 0
DWIDTH 5 0
BBX 3 7 1 0
BITMAP
a0
a0
a0
a0
a0
a0
a0
ENDCHAR
STARTCHAR backslash2
ENCODING 116
SWIDTH 250 0
DWIDTH 8 0
BBX 6 11 1 -2
BITMAP
80
c0
c0
60
60
30
30
18
18
0c
0c
ENDCHAR
STARTCHAR backslash3
ENCODING 117
SWIDTH 250 0
DWIDTH 7 0
BBX 5 8 1 0
BITMAP
00
80
80
40
20
10
08
08
ENDCHAR
STARTCHAR diagonaldots
ENCODING 118
SWIDTH 250 0
DWIDTH 9 0
BBX 7 10 1 -1
BITMAP
80
80
00
00
10
10
00
00
02
02
ENDCHAR
STARTCHAR simequal
ENCODING 119
SWIDTH 549 0
DWIDTH 8 0
BBX 6 6 1 0
BITMAP
64
b4
98
00
00
fc
ENDCHAR
STARTCHAR florin
ENCODING 120
SWIDTH 500 0
DWIDTH 8 0
BBX 7 9 1 -2
BITMAP
3e
30
30
60
78
60
c0
c0
c0
ENDCHAR
STARTCHAR asym
ENCODING 121
SWIDTH 250 0
DWIDTH 10 0
BBX 8 7 1 0
BITMAP
81
42
3c
00
3c
42
81
ENDCHAR
STARTCHAR minusplus
ENCODING 122
SWIDTH 250 0
DWIDTH 7 0
BBX 5 9 1 0
BITMAP
00
00
f8
00
20
20
f8
20
20
ENDCHAR
STARTCHAR less2
ENCODING 123
SWIDTH 549 0
DWIDTH 7 0
BBX 6 5 0 1
BITMAP
0c
30
c0
30
0c
ENDCHAR
STARTCHAR bowtie
ENCODING 124
SWIDTH 250 0
DWIDTH 9 0
BBX 7 5 1 2
BITMAP
c6
aa
92
aa
c6
ENDCHAR
STARTCHAR greater2
ENCODING 125
SWIDTH 549 0
DWIDTH 7 0
BBX 6 5 0 1
BITMAP
c0
30
0c
30
c0
ENDCHAR
STARTCHAR centraldots
ENCODING 126
SWIDTH 1000 0
DWIDTH 11 0
BBX 9 2 1 3
BITMAP
8880
8880
ENDCHAR
STARTCHAR visiblespace
ENCODING 160
SWIDTH 250 0
DWIDTH 7 0
BBX 5 3 1 -1
BITMAP
00
88
f8
ENDCHAR
STARTCHAR dagger1
ENCODING 161
SWIDTH 250 0
DWIDTH 7 0
BBX 5 8 1 0
BITMAP
20
20
f8
20
20
70
20
20
ENDCHAR
STARTCHAR circledot
ENCODING 162
SWIDTH 768 0
DWIDTH 9 0
BBX 7 7 1 0
BITMAP
38
44
82
92
82
44
38
ENDCHAR
STARTCHAR propersqsuperset
ENCODING 163
SWIDTH 713 0
DWIDTH 9 0
BBX 7 6 1 1
BITMAP
fe
02
02
02
02
fe
ENDCHAR
STARTCHAR reflexsqsuperset
ENCODING 164
SWIDTH 713 0
DWIDTH 9 0
BBX 7 8 1 0
BITMAP
fe
02
02
02
02
fe
00
fe
ENDCHAR
STARTCHAR gradient1
ENCODING 165
SWIDTH 713 0
DWIDTH 8 0
BBX 6 6 1 1
BITMAP
fc
84
84
48
48
30
ENDCHAR
STARTCHAR propersqsubset
ENCODING 166
SWIDTH 713 0
DWIDTH 9 0
BBX 7 6 1 1
BITMAP
fe
80
80
80
80
fe
ENDCHAR
STARTCHAR reflexsqsubset
ENCODING 167
SWIDTH 713 0
DWIDTH 9 0
BBX 7 8 1 0
BITMAP
fe
80
80
80
80
fe
00
fe
ENDCHAR
STARTCHAR smalllozenge
ENCODING 168
SWIDTH 494 0
DWIDTH 9 0
BBX 7 7 1 1
BITMAP
10
28
44
82
44
28
10
ENDCHAR
STARTCHAR lessless
ENCODING 169
SWIDTH 549 0
DWIDTH 12 0
BBX 10 7 1 0
BITMAP
0440
1980
6600
8800
6600
1980
0440
ENDCHAR
STARTCHAR greatergreater
ENCODING 170
SWIDTH 549 0
DWIDTH 12 0
BBX 10 7 1 0
BITMAP
8800
6600
1980
0440
1980
6600
8800
ENDCHAR
STARTCHAR unionplus
ENCODING 171
SWIDTH 768 0
DWIDTH 9 0
BBX 7 6 1 1
BITMAP
92
92
fe
92
54
38
ENDCHAR
STARTCHAR sqintersection
ENCODING 172
SWIDTH 768 0
DWIDTH 9 0
BBX 7 6 1 1
BITMAP
fe
82
82
82
82
82
ENDCHAR
STARTCHAR squnion
ENCODING 173
SWIDTH 768 0
DWIDTH 9 0
BBX 7 6 1 1
BITMAP
82
82
82
82
82
fe
ENDCHAR
STARTCHAR frown
ENCODING 174
SWIDTH 250 0
DWIDTH 10 0
BBX 8 3 1 2
BITMAP
3c
42
81
ENDCHAR
STARTCHAR smile
ENCODING 175
SWIDTH 250 0
DWIDTH 10 0
BBX 8 3 1 2
BITMAP
81
42
3c
ENDCHAR
STARTCHAR reflexprec
ENCODING 176
SWIDTH 549 0
DWIDTH 8 0
BBX 6 9 1 -1
BITMAP
04
04
18
e0
18
04
04
00
fc
ENDCHAR
STARTCHAR reflexsucc
ENCODING 177
SWIDTH 549 0
DWIDTH 8 0
BBX 6 9 1 -1
BITMAP
80
80
60
1c
60
80
80
00
fc
ENDCHAR
STARTCHAR properprec
ENCODING 178
SWIDTH 549 0
DWIDTH 8 0
BBX 6 7 1 0
BITMAP
04
04
18
e0
18
04
04
ENDCHAR
STARTCHAR propersucc
ENCODING 179
SWIDTH 549 0
DWIDTH 8 0
BBX 6 7 1 0
BITMAP
80
80
60
1c
60
80
80
ENDCHAR
STARTCHAR bardash
ENCODING 180
SWIDTH 494 0
DWIDTH 8 0
BBX 6 7 1 0
BITMAP
80
80
80
fc
80
80
80
ENDCHAR
STARTCHAR dashbar
ENCODING 181
SWIDTH 494 0
DWIDTH 8 0
BBX 6 7 1 0
BITMAP
04
04
04
fc
04
04
04
ENDCHAR
STARTCHAR bardashdbl
ENCODING 182
SWIDTH 494 0
DWIDTH 8 0
BBX 6 7 1 0
BITMAP
80
80
fc
80
fc
80
80
ENDCHAR
STARTCHAR smallintegral
ENCODING 183
SWIDTH 274 0
DWIDTH 7 0
BBX 5 9 1 0
BITMAP
18
28
20
20
20
20
20
a0
c0
ENDCHAR
STARTCHAR circleintegral
ENCODING 184
SWIDTH 274 0
DWIDTH 8 0
BBX 6 11 1 -2
BITMAP
1c
34
30
78
b4
b4
b4
78
30
b0
e0
ENDCHAR
STARTCHAR coproduct
ENCODING 185
SWIDTH 823 0
DWIDTH 11 0
BBX 9 11 1 -2
BITMAP
e380
6300
6300
6300
6300
6300
6300
6300
6300
6300
ff80
ENDCHAR
STARTCHAR bigcircledot
ENCODING 186
SWIDTH 768 0
DWIDTH 11 0
BBX 9 9 1 -1
BITMAP
3e00
7f00
e380
c180
c980
c180
e380
7f00
3e00
ENDCHAR
STARTCHAR bigcirclemultiply
ENCODING 187
SWIDTH 768 0
DWIDTH 11 0
BBX 9 9 1 -1
BITMAP
3e00
7f00
e380
d580
c980
d580
e380
7f00
3e00
ENDCHAR
STARTCHAR bigcircleplus
ENCODING 188
SWIDTH 768 0
DWIDTH 11 0
BBX 9 9 1 -1
BITMAP
3e00
7f00
eb80
c980
ff80
c980
eb80
7f00
3e00
ENDCHAR
STARTCHAR biglogicaland
ENCODING 189
SWIDTH 603 0
DWIDTH 11 0
BBX 9 11 1 -2
BITMAP
1c00
1c00
3600
3600
3600
6300
6300
6300
c180
c180
c180
ENDCHAR
STARTCHAR biglogicalor
ENCODING 190
SWIDTH 603 0
DWIDTH 11 0
BBX 9 11 1 -2
BITMAP
c180
c180
c180
6300
6300
6300
3600
3600
3600
1c00
1c00
ENDCHAR
STARTCHAR bigintersection
ENCODING 191
SWIDTH 603 0
DWIDTH 11 0
BBX 9 11 1 -2
BITMAP
3e00
6300
c180
c180
c180
c180
c180
c180
c180
c180
c180
ENDCHAR
STARTCHAR bigunion
ENCODING 192
SWIDTH 603 0
DWIDTH 11 0
BBX 9 11 1 -2
BITMAP
c180
c180
c180
c180
c180
c180
c180
c180
c180
6300
3e00
ENDCHAR
STARTCHAR bigunionplus
ENCODING 193
SWIDTH 603 0
DWIDTH 11 0
BBX 9 11 1 -2
BITMAP
c180
c180
c180
c980
c980
ff80
c980
c980
c180
6300
3e00
ENDCHAR
STARTCHAR bigsqunion
ENCODING 194
SWIDTH 603 0
DWIDTH 11 0
BBX 9 11 1 -2
BITMAP
c180
c180
c180
c180
c180
c180
c180
c180
c180
c180
ff80
ENDCHAR
STARTCHAR bigcircle
ENCODING 195
SWIDTH 768 0
DWIDTH 11 0
BBX 9 9 1 0
BITMAP
3e00
6300
c180
8080
8080
8080
c180
6300
3e00
ENDCHAR
STARTCHAR guilsinglleft
ENCODING 196
SWIDTH 250 0
DWIDTH 5 0
BBX 3 5 1 1
BITMAP
20
40
80
40
20
ENDCHAR
STARTCHAR circleminus
ENCODING 197
SWIDTH 768 0
DWIDTH 9 0
BBX 7 7 1 0
BITMAP
38
44
82
fe
82
44
38
ENDCHAR
STARTCHAR smalltriangleleft
ENCODING 198
SWIDTH 713 0
DWIDTH 8 0
BBX 6 6 1 1
BITMAP
1c
64
84
84
64
1c
ENDCHAR
STARTCHAR perthousand
ENCODING 199
SWIDTH 1000 0
DWIDTH 14 0
BBX 13 8 0 0
BITMAP
6200
9400
9400
6800
0b30
14c8
14c8
2330
ENDCHAR
STARTCHAR existential1
ENCODING 200
SWIDTH 549 0
DWIDTH 7 0
BBX 5 9 1 0
BITMAP
f8
08
08
08
f8
08
08
08
f8
ENDCHAR
STARTCHAR daggerdbl1
ENCODING 201
SWIDTH 250 0
DWIDTH 7 0
BBX 5 8 1 0
BITMAP
20
f8
20
70
70
20
f8
20
ENDCHAR
STARTCHAR daggerdbl
ENCODING 202
SWIDTH 250 0
DWIDTH 7 0
BBX 5 11 1 -2
BITMAP
20
a8
f8
20
70
20
70
20
f8
a8
20
ENDCHAR
STARTCHAR bigbowtie
ENCODING 203
SWIDTH 250 0
DWIDTH 11 0
BBX 9 7 1 1
BITMAP
c180
a280
9480
8880
9480
a280
c180
ENDCHAR
STARTCHAR circ
ENCODING 204
SWIDTH 460 0
DWIDTH 6 0
BBX 4 4 1 2
BITMAP
60
90
90
60
ENDCHAR
STARTCHAR grave
ENCODING 205
SWIDTH 333 0
DWIDTH 4 0
BBX 2 2 1 7
BITMAP
80
40
ENDCHAR
STARTCHAR circumflex
ENCODING 206
SWIDTH 333 0
DWIDTH 5 0
BBX 3 2 1 7
BITMAP
40
a0
ENDCHAR
STARTCHAR tilde
ENCODING 207
SWIDTH 333 0
DWIDTH 7 0
BBX 5 2 1 7
BITMAP
68
b0
ENDCHAR
STARTCHAR longarrowboth
ENCODING 208
SWIDTH 987 0
DWIDTH 19 0
BBX 17 5 1 1
BITMAP
200200
400100
ffff80
400100
200200
ENDCHAR
STARTCHAR endash
ENCODING 209
SWIDTH 556 0
DWIDTH 8 0
BBX 8 1 0 3
BITMAP
ff
ENDCHAR
STARTCHAR emdash
ENCODING 210
SWIDTH 1000 0
DWIDTH 14 0
BBX 14 1 0 3
BITMAP
fffc
ENDCHAR
STARTCHAR Ydiaeresis
ENCODING 211
SWIDTH 667 0
DWIDTH 9 0
BBX 7 11 1 0
BITMAP
28
00
82
82
44
44
28
10
10
10
10
ENDCHAR
STARTCHAR ampersand2
ENCODING 212
SWIDTH 778 0
DWIDTH 10 0
BBX 9 9 1 0
BITMAP
3000
4800
4800
3700
7200
9a00
8c00
8c80
7300
ENDCHAR
STARTCHAR universal1
ENCODING 213
SWIDTH 713 0
DWIDTH 9 0
BBX 9 9 0 0
BITMAP
8080
4100
4100
3e00
2200
1400
1400
0800
0800
ENDCHAR
STARTCHAR booleans
ENCODING 214
SWIDTH 667 0
DWIDTH 11 0
BBX 9 9 1 0
BITMAP
ff00
5380
5280
5380
5f00
5280
5280
5380
ff00
ENDCHAR
STARTCHAR complexnums
ENCODING 215
SWIDTH 722 0
DWIDTH 9 0
BBX 7 9 1 0
BITMAP
3a
66
a2
a0
a0
a0
a0
62
3e
ENDCHAR
STARTCHAR natnums
ENCODING 216
SWIDTH 722 0
DWIDTH 10 0
BBX 8 9 1 0
BITMAP
e7
72
5a
6e
76
5a
4e
46
e2
ENDCHAR
STARTCHAR rationalnums
ENCODING 217
SWIDTH 722 0
DWIDTH 10 0
BBX 8 10 1 -1
BITMAP
3c
66
a5
a5
a5
a5
a5
66
3c
0f
ENDCHAR
STARTCHAR realnums
ENCODING 218
SWIDTH 667 0
DWIDTH 11 0
BBX 9 9 1 0
BITMAP
ff00
5380
5280
5380
5f00
5a00
5500
5580
f380
ENDCHAR
STARTCHAR integers
ENCODING 219
SWIDTH 611 0
DWIDTH 9 0
BBX 7 9 1 0
BITMAP
fe
96
34
2c
68
58
d2
a6
fe
ENDCHAR
STARTCHAR lesssim
ENCODING 220
SWIDTH 549 0
DWIDTH 8 0
BBX 6 8 1 0
BITMAP
0c
30
c0
30
0c
00
64
98
ENDCHAR
STARTCHAR greatersim
ENCODING 221
SWIDTH 549 0
DWIDTH 8 0
BBX 6 8 1 0
BITMAP
c0
30
0c
30
c0
00
64
98
ENDCHAR
STARTCHAR lessapprox
ENCODING 222
SWIDTH 549 0
DWIDTH 8 0
BBX 6 11 1 -2
BITMAP
0c
30
c0
30
0c
00
64
98
00
64
98
ENDCHAR
STARTCHAR greaterapprox
ENCODING 223
SWIDTH 549 0
DWIDTH 8 0
BBX 6 11 1 -2
BITMAP
c0
30
0c
30
c0
00
64
98
00
64
98
ENDCHAR
STARTCHAR definedas
ENCODING 224
SWIDTH 549 0
DWIDTH 7 0
BBX 5 7 1 1
BITMAP
20
50
f8
00
f8
00
f8
ENDCHAR
STARTCHAR circleminus1
ENCODING 225
SWIDTH 768 0
DWIDTH 9 0
BBX 7 7 1 0
BITMAP
38
44
82
ba
82
44
38
ENDCHAR
STARTCHAR circleasterisk
ENCODING 226
SWIDTH 768 0
DWIDTH 9 0
BBX 7 7 1 0
BITMAP
38
54
d6
ba
d6
54
38
ENDCHAR
STARTCHAR circlecirc
ENCODING 227
SWIDTH 768 0
DWIDTH 9 0
BBX 7 7 1 0
BITMAP
38
44
ba
aa
ba
44
38
ENDCHAR
STARTCHAR dollar1
ENCODING 228
SWIDTH 556 0
DWIDTH 8 0
BBX 7 11 0 -1
BITMAP
28
7c
aa
a8
a8
7c
2a
2a
aa
7c
28
ENDCHAR
STARTCHAR euro
ENCODING 229
SWIDTH 722 0
DWIDTH 10 0
BBX 8 9 1 -1
BITMAP
1e
21
40
fe
40
fc
40
21
1e
ENDCHAR
STARTCHAR therefore1
ENCODING 230
SWIDTH 863 0
DWIDTH 9 0
BBX 7 6 1 0
BITMAP
10
10
00
00
82
82
ENDCHAR
STARTCHAR coloncolon
ENCODING 231
SWIDTH 863 0
DWIDTH 6 0
BBX 4 6 1 0
BITMAP
90
90
00
00
90
90
ENDCHAR
STARTCHAR bigsqintersection
ENCODING 232
SWIDTH 603 0
DWIDTH 11 0
BBX 9 11 1 -2
BITMAP
ff80
c180
c180
c180
c180
c180
c180
c180
c180
c180
c180
ENDCHAR
STARTCHAR semanticsleft
ENCODING 233
SWIDTH 863 0
DWIDTH 6 0
BBX 5 11 1 -2
BITMAP
f8
a0
a0
a0
a0
a0
a0
a0
a0
a0
f8
ENDCHAR
STARTCHAR semanticsright
ENCODING 234
SWIDTH 863 0
DWIDTH 6 0
BBX 5 11 0 -2
BITMAP
f8
28
28
28
28
28
28
28
28
28
f8
ENDCHAR
STARTCHAR doubleparenleft
ENCODING 235
SWIDTH 1000 0
DWIDTH 6 0
BBX 4 11 1 -2
BITMAP
30
50
50
90
90
90
90
90
50
50
30
ENDCHAR
STARTCHAR doubleparenright
ENCODING 236
SWIDTH 1000 0
DWIDTH 6 0
BBX 4 11 1 -2
BITMAP
c0
a0
a0
90
90
90
90
90
a0
a0
c0
ENDCHAR
ENDFONT
isabelle