Dear ProofPower Users,
For those who use ProofPower on a laptop with a smaller screen, I
attached a font that is a bit more compact than Holnormal18 but not as
small as Holsans10. It has a height of 14 pixels, and indeed most
special characters are just adapted from Holnormal18.
To install, just copy the attached bitmap font file into the fonts
directory of the ProofPower installation, and change holnormal into
holcompact in your Xpp configuration file (app-defaults folder).
All the Best
Frank
--
Frank Zeyda, BSc Dipl.-Inform. PhD
Research Associate
High Integrity Systems Engineering Group
Department of Computer Science
University of York (UK)
Email: ze...@cs.york.ac.uk
Phone: +44-(0)1904-325434
WWW: http://www-users.cs.york.ac.uk/~zeyda/
EMAIL DISCLAIMER: http://www.york.ac.uk/docs/disclaimer/email.htm
STARTFONT 2.1
COMMENT FONT -Adobe-Courier-Medium-R-Normal--14-140-75-75-M-90-ISO8859-1
FONT holcompact
SIZE 14 75 75
FONTBOUNDINGBOX 14 15 -1 -3
STARTPROPERTIES 29
FOUNDRY "Adobe"
FAMILY_NAME "Courier"
WEIGHT_NAME "Medium"
SLANT "R"
SETWIDTH_NAME "Normal"
ADD_STYLE_NAME ""
PIXEL_SIZE 14
POINT_SIZE 140
RESOLUTION_X 75
RESOLUTION_Y 75
SPACING "P"
AVERAGE_WIDTH 90
CHARSET_REGISTRY "ISO8859"
CHARSET_ENCODING "1"
CAP_HEIGHT 9
X_HEIGHT 7
FACE_NAME "Courier"
NOTICE "No mark"
_DEC_DEVICE_FONTNAMES "PS=Courier"
RELATIVE_SETWIDTH 50
RELATIVE_WEIGHT 50
FULL_NAME "Courier"
WEIGHT 10
QUAD_WIDTH 9
DEFAULT_CHAR 0
FONT_DESCENT 3
FONT_ASCENT 12
_GBDFED_INFO "Edited with gbdfed 1.5."
ENDPROPERTIES
CHARS 223
STARTCHAR space
ENCODING 32
SWIDTH 548 0
DWIDTH 8 0
BBX 0 0 0 0
BITMAP
ENDCHAR
STARTCHAR exclam
ENCODING 33
SWIDTH 480 0
DWIDTH 7 0
BBX 1 10 2 0
BITMAP
80
80
80
80
80
80
80
00
00
80
ENDCHAR
STARTCHAR quotedbl
ENCODING 34
SWIDTH 685 0
DWIDTH 10 0
BBX 4 4 2 5
BITMAP
90
90
90
90
ENDCHAR
STARTCHAR numbersign
ENCODING 35
SWIDTH 617 0
DWIDTH 9 0
BBX 5 9 1 0
BITMAP
50
50
50
F8
50
F8
50
50
50
ENDCHAR
STARTCHAR dollar
ENCODING 36
SWIDTH 480 0
DWIDTH 7 0
BBX 5 13 0 -2
BITMAP
20
20
78
88
80
C0
30
08
88
F0
20
20
20
ENDCHAR
STARTCHAR percent
ENCODING 37
SWIDTH 617 0
DWIDTH 9 0
BBX 7 10 0 0
BITMAP
60
90
90
66
18
30
CC
12
12
0C
ENDCHAR
STARTCHAR ampersand
ENCODING 38
SWIDTH 685 0
DWIDTH 10 0
BBX 6 8 1 0
BITMAP
38
48
40
40
A8
90
98
64
ENDCHAR
STARTCHAR quotesingle
ENCODING 39
SWIDTH 274 0
DWIDTH 4 0
BBX 2 4 0 6
BITMAP
40
40
40
80
ENDCHAR
STARTCHAR parenleft
ENCODING 40
SWIDTH 480 0
DWIDTH 7 0
BBX 3 12 1 -2
BITMAP
20
40
40
80
80
80
80
80
80
40
40
20
ENDCHAR
STARTCHAR parenright
ENCODING 41
SWIDTH 480 0
DWIDTH 7 0
BBX 3 12 1 -2
BITMAP
80
40
40
20
20
20
20
20
20
40
40
80
ENDCHAR
STARTCHAR asterisk
ENCODING 42
SWIDTH 617 0
DWIDTH 9 0
BBX 5 6 1 3
BITMAP
20
20
F8
20
50
88
ENDCHAR
STARTCHAR plus
ENCODING 43
SWIDTH 754 0
DWIDTH 11 0
BBX 7 7 1 1
BITMAP
10
10
10
FE
10
10
10
ENDCHAR
STARTCHAR comma
ENCODING 44
SWIDTH 685 0
DWIDTH 10 0
BBX 3 4 2 -2
BITMAP
60
60
C0
80
ENDCHAR
STARTCHAR hyphen
ENCODING 45
SWIDTH 685 0
DWIDTH 10 0
BBX 6 1 1 4
BITMAP
FC
ENDCHAR
STARTCHAR period
ENCODING 46
SWIDTH 548 0
DWIDTH 8 0
BBX 2 2 2 0
BITMAP
C0
C0
ENDCHAR
STARTCHAR slash
ENCODING 47
SWIDTH 685 0
DWIDTH 10 0
BBX 6 11 1 -1
BITMAP
04
08
08
10
10
20
20
40
40
80
80
ENDCHAR
STARTCHAR zero
ENCODING 48
SWIDTH 548 0
DWIDTH 8 0
BBX 6 10 0 0
BITMAP
78
84
84
84
84
84
84
84
84
78
ENDCHAR
STARTCHAR one
ENCODING 49
SWIDTH 480 0
DWIDTH 7 0
BBX 5 10 0 0
BITMAP
20
60
A0
20
20
20
20
20
20
F8
ENDCHAR
STARTCHAR two
ENCODING 50
SWIDTH 548 0
DWIDTH 8 0
BBX 6 10 0 0
BITMAP
78
84
84
04
08
10
20
40
84
FC
ENDCHAR
STARTCHAR three
ENCODING 51
SWIDTH 548 0
DWIDTH 8 0
BBX 6 10 0 0
BITMAP
78
84
04
04
38
04
04
04
84
78
ENDCHAR
STARTCHAR four
ENCODING 52
SWIDTH 548 0
DWIDTH 8 0
BBX 6 10 0 0
BITMAP
18
28
28
48
48
88
88
FC
08
1C
ENDCHAR
STARTCHAR five
ENCODING 53
SWIDTH 548 0
DWIDTH 8 0
BBX 6 10 0 0
BITMAP
7C
40
40
40
78
04
04
04
84
78
ENDCHAR
STARTCHAR six
ENCODING 54
SWIDTH 548 0
DWIDTH 8 0
BBX 6 10 0 0
BITMAP
38
40
80
80
B8
C4
84
84
44
38
ENDCHAR
STARTCHAR seven
ENCODING 55
SWIDTH 548 0
DWIDTH 8 0
BBX 6 10 0 0
BITMAP
FC
84
04
08
08
08
10
10
10
10
ENDCHAR
STARTCHAR eight
ENCODING 56
SWIDTH 548 0
DWIDTH 8 0
BBX 6 10 0 0
BITMAP
78
84
84
84
78
84
84
84
84
78
ENDCHAR
STARTCHAR nine
ENCODING 57
SWIDTH 548 0
DWIDTH 8 0
BBX 6 10 0 0
BITMAP
70
88
84
84
8C
74
04
04
08
70
ENDCHAR
STARTCHAR colon
ENCODING 58
SWIDTH 548 0
DWIDTH 8 0
BBX 2 7 2 0
BITMAP
C0
C0
00
00
00
C0
C0
ENDCHAR
STARTCHAR semicolon
ENCODING 59
SWIDTH 685 0
DWIDTH 10 0
BBX 3 9 2 -2
BITMAP
60
60
00
00
00
60
60
C0
80
ENDCHAR
STARTCHAR less
ENCODING 60
SWIDTH 754 0
DWIDTH 11 0
BBX 7 7 1 1
BITMAP
06
18
60
80
60
18
06
ENDCHAR
STARTCHAR equal
ENCODING 61
SWIDTH 754 0
DWIDTH 11 0
BBX 7 3 1 3
BITMAP
FE
00
FE
ENDCHAR
STARTCHAR greater
ENCODING 62
SWIDTH 754 0
DWIDTH 11 0
BBX 7 7 1 1
BITMAP
C0
30
0C
02
0C
30
C0
ENDCHAR
STARTCHAR question
ENCODING 63
SWIDTH 480 0
DWIDTH 7 0
BBX 5 9 0 0
BITMAP
70
88
88
08
10
20
20
00
20
ENDCHAR
STARTCHAR at
ENCODING 64
SWIDTH 754 0
DWIDTH 11 0
BBX 7 10 1 -1
BITMAP
38
44
84
9C
A4
A4
9E
80
40
38
ENDCHAR
STARTCHAR A
ENCODING 65
SWIDTH 754 0
DWIDTH 11 0
BBX 9 9 0 0
BITMAP
3800
0800
1400
1400
2200
3E00
4100
4100
F780
ENDCHAR
STARTCHAR B
ENCODING 66
SWIDTH 617 0
DWIDTH 9 0
BBX 7 9 0 0
BITMAP
FC
42
42
42
7C
42
42
42
FC
ENDCHAR
STARTCHAR C
ENCODING 67
SWIDTH 617 0
DWIDTH 9 0
BBX 7 9 0 0
BITMAP
3A
46
82
80
80
80
80
42
3C
ENDCHAR
STARTCHAR D
ENCODING 68
SWIDTH 685 0
DWIDTH 10 0
BBX 8 9 0 0
BITMAP
FC
42
41
41
41
41
41
42
FC
ENDCHAR
STARTCHAR E
ENCODING 69
SWIDTH 617 0
DWIDTH 9 0
BBX 7 9 0 0
BITMAP
FE
42
42
48
78
48
42
42
FE
ENDCHAR
STARTCHAR F
ENCODING 70
SWIDTH 617 0
DWIDTH 9 0
BBX 7 9 0 0
BITMAP
FE
42
42
48
78
48
40
40
F0
ENDCHAR
STARTCHAR G
ENCODING 71
SWIDTH 685 0
DWIDTH 10 0
BBX 8 9 0 0
BITMAP
3A
46
82
80
80
8F
82
42
3C
ENDCHAR
STARTCHAR H
ENCODING 72
SWIDTH 685 0
DWIDTH 10 0
BBX 8 9 0 0
BITMAP
E7
42
42
42
7E
42
42
42
E7
ENDCHAR
STARTCHAR I
ENCODING 73
SWIDTH 480 0
DWIDTH 7 0
BBX 5 9 0 0
BITMAP
F8
20
20
20
20
20
20
20
F8
ENDCHAR
STARTCHAR J
ENCODING 74
SWIDTH 617 0
DWIDTH 9 0
BBX 7 9 0 0
BITMAP
3E
08
08
08
08
88
88
88
70
ENDCHAR
STARTCHAR K
ENCODING 75
SWIDTH 685 0
DWIDTH 10 0
BBX 8 9 0 0
BITMAP
EE
44
48
50
70
48
44
44
E3
ENDCHAR
STARTCHAR L
ENCODING 76
SWIDTH 685 0
DWIDTH 10 0
BBX 8 9 0 0
BITMAP
F8
20
20
20
20
21
21
21
FF
ENDCHAR
STARTCHAR M
ENCODING 77
SWIDTH 754 0
DWIDTH 11 0
BBX 9 9 0 0
BITMAP
E380
6300
5700
5500
4900
4900
4100
4100
E380
ENDCHAR
STARTCHAR N
ENCODING 78
SWIDTH 685 0
DWIDTH 10 0
BBX 8 9 0 0
BITMAP
E7
62
52
52
4A
4A
46
46
E2
ENDCHAR
STARTCHAR O
ENCODING 79
SWIDTH 685 0
DWIDTH 10 0
BBX 8 9 0 0
BITMAP
3C
42
81
81
81
81
81
42
3C
ENDCHAR
STARTCHAR P
ENCODING 80
SWIDTH 617 0
DWIDTH 9 0
BBX 7 9 0 0
BITMAP
FC
42
42
42
42
7C
40
40
F0
ENDCHAR
STARTCHAR Q
ENCODING 81
SWIDTH 685 0
DWIDTH 10 0
BBX 8 11 0 -2
BITMAP
3C
42
81
81
81
81
81
42
3C
31
5E
ENDCHAR
STARTCHAR R
ENCODING 82
SWIDTH 685 0
DWIDTH 10 0
BBX 8 9 0 0
BITMAP
FC
42
42
42
44
78
44
42
E1
ENDCHAR
STARTCHAR S
ENCODING 83
SWIDTH 548 0
DWIDTH 8 0
BBX 6 9 0 0
BITMAP
74
8C
84
80
78
04
84
C4
B8
ENDCHAR
STARTCHAR T
ENCODING 84
SWIDTH 617 0
DWIDTH 9 0
BBX 7 9 0 0
BITMAP
FE
92
92
10
10
10
10
10
7C
ENDCHAR
STARTCHAR U
ENCODING 85
SWIDTH 685 0
DWIDTH 10 0
BBX 8 9 0 0
BITMAP
E7
42
42
42
42
42
42
42
3C
ENDCHAR
STARTCHAR V
ENCODING 86
SWIDTH 754 0
DWIDTH 11 0
BBX 9 9 0 0
BITMAP
E380
4100
4100
2200
2200
1400
1400
0800
0800
ENDCHAR
STARTCHAR W
ENCODING 87
SWIDTH 754 0
DWIDTH 11 0
BBX 9 9 0 0
BITMAP
E380
4100
4900
4900
5500
5500
2200
2200
2200
ENDCHAR
STARTCHAR X
ENCODING 88
SWIDTH 685 0
DWIDTH 10 0
BBX 8 9 0 0
BITMAP
E7
42
24
24
18
24
24
42
E7
ENDCHAR
STARTCHAR Y
ENCODING 89
SWIDTH 617 0
DWIDTH 9 0
BBX 7 9 0 0
BITMAP
EE
44
44
28
28
10
10
10
7C
ENDCHAR
STARTCHAR Z
ENCODING 90
SWIDTH 548 0
DWIDTH 8 0
BBX 6 9 0 0
BITMAP
FC
84
88
10
20
20
44
84
FC
ENDCHAR
STARTCHAR bracketleft
ENCODING 91
SWIDTH 617 0
DWIDTH 9 0
BBX 3 12 2 -2
BITMAP
E0
80
80
80
80
80
80
80
80
80
80
E0
ENDCHAR
STARTCHAR backslash
ENCODING 92
SWIDTH 685 0
DWIDTH 10 0
BBX 6 11 1 -1
BITMAP
80
40
40
20
20
10
10
08
08
04
04
ENDCHAR
STARTCHAR bracketright
ENCODING 93
SWIDTH 617 0
DWIDTH 9 0
BBX 3 12 2 -2
BITMAP
E0
20
20
20
20
20
20
20
20
20
20
E0
ENDCHAR
STARTCHAR asciicircum
ENCODING 94
SWIDTH 617 0
DWIDTH 9 0
BBX 5 5 1 4
BITMAP
20
50
50
88
88
ENDCHAR
STARTCHAR underscore
ENCODING 95
SWIDTH 754 0
DWIDTH 11 0
BBX 9 1 0 -1
BITMAP
FF80
ENDCHAR
STARTCHAR grave
ENCODING 96
SWIDTH 274 0
DWIDTH 4 0
BBX 2 4 0 6
BITMAP
80
80
80
40
ENDCHAR
STARTCHAR a
ENCODING 97
SWIDTH 617 0
DWIDTH 9 0
BBX 7 7 0 0
BITMAP
78
84
04
7C
84
8C
76
ENDCHAR
STARTCHAR b
ENCODING 98
SWIDTH 685 0
DWIDTH 10 0
BBX 8 10 0 0
BITMAP
C0
40
40
5C
62
41
41
41
62
DC
ENDCHAR
STARTCHAR c
ENCODING 99
SWIDTH 617 0
DWIDTH 9 0
BBX 7 7 0 0
BITMAP
3A
46
82
80
80
42
3C
ENDCHAR
STARTCHAR d
ENCODING 100
SWIDTH 685 0
DWIDTH 10 0
BBX 8 10 0 0
BITMAP
06
02
02
3A
46
82
82
82
46
3B
ENDCHAR
STARTCHAR e
ENCODING 101
SWIDTH 617 0
DWIDTH 9 0
BBX 7 7 0 0
BITMAP
38
44
82
FE
80
42
3C
ENDCHAR
STARTCHAR f
ENCODING 102
SWIDTH 617 0
DWIDTH 9 0
BBX 7 10 0 0
BITMAP
1E
20
20
FC
20
20
20
20
20
F8
ENDCHAR
STARTCHAR g
ENCODING 103
SWIDTH 685 0
DWIDTH 10 0
BBX 8 10 0 -3
BITMAP
3B
46
82
82
82
46
3A
02
04
78
ENDCHAR
STARTCHAR h
ENCODING 104
SWIDTH 685 0
DWIDTH 10 0
BBX 8 10 0 0
BITMAP
C0
40
40
5C
62
42
42
42
42
E7
ENDCHAR
STARTCHAR i
ENCODING 105
SWIDTH 480 0
DWIDTH 7 0
BBX 5 10 0 0
BITMAP
20
20
00
E0
20
20
20
20
20
F8
ENDCHAR
STARTCHAR j
ENCODING 106
SWIDTH 480 0
DWIDTH 7 0
BBX 5 13 0 -3
BITMAP
10
10
00
F8
08
08
08
08
08
08
08
10
E0
ENDCHAR
STARTCHAR k
ENCODING 107
SWIDTH 617 0
DWIDTH 9 0
BBX 7 9 0 0
BITMAP
C0
40
4E
48
50
60
50
48
CE
ENDCHAR
STARTCHAR l
ENCODING 108
SWIDTH 480 0
DWIDTH 7 0
BBX 5 9 0 0
BITMAP
E0
20
20
20
20
20
20
20
F8
ENDCHAR
STARTCHAR m
ENCODING 109
SWIDTH 685 0
DWIDTH 10 0
BBX 9 7 -1 0
BITMAP
DB00
6D00
4900
4900
4900
4900
ED80
ENDCHAR
STARTCHAR n
ENCODING 110
SWIDTH 685 0
DWIDTH 10 0
BBX 8 7 0 0
BITMAP
DC
62
42
42
42
42
E7
ENDCHAR
STARTCHAR o
ENCODING 111
SWIDTH 685 0
DWIDTH 10 0
BBX 8 7 0 0
BITMAP
3C
42
81
81
81
42
3C
ENDCHAR
STARTCHAR p
ENCODING 112
SWIDTH 685 0
DWIDTH 10 0
BBX 8 10 0 -3
BITMAP
DC
62
41
41
41
62
5C
40
40
F0
ENDCHAR
STARTCHAR q
ENCODING 113
SWIDTH 685 0
DWIDTH 10 0
BBX 8 10 0 -3
BITMAP
3B
46
82
82
82
46
3A
02
02
0F
ENDCHAR
STARTCHAR r
ENCODING 114
SWIDTH 617 0
DWIDTH 9 0
BBX 7 7 0 0
BITMAP
CC
52
60
40
40
40
F0
ENDCHAR
STARTCHAR s
ENCODING 115
SWIDTH 548 0
DWIDTH 8 0
BBX 6 7 0 0
BITMAP
7C
84
80
78
04
84
F8
ENDCHAR
STARTCHAR t
ENCODING 116
SWIDTH 548 0
DWIDTH 8 0
BBX 6 9 0 0
BITMAP
40
40
F8
40
40
40
40
44
38
ENDCHAR
STARTCHAR u
ENCODING 117
SWIDTH 685 0
DWIDTH 10 0
BBX 8 7 0 0
BITMAP
C6
42
42
42
42
46
3B
ENDCHAR
STARTCHAR v
ENCODING 118
SWIDTH 685 0
DWIDTH 10 0
BBX 8 7 0 0
BITMAP
E7
42
42
24
24
18
18
ENDCHAR
STARTCHAR w
ENCODING 119
SWIDTH 754 0
DWIDTH 11 0
BBX 9 7 0 0
BITMAP
E380
4100
4900
4900
2A00
3600
3600
ENDCHAR
STARTCHAR x
ENCODING 120
SWIDTH 617 0
DWIDTH 9 0
BBX 7 7 0 0
BITMAP
EE
44
28
10
28
44
EE
ENDCHAR
STARTCHAR y
ENCODING 121
SWIDTH 685 0
DWIDTH 10 0
BBX 8 10 0 -3
BITMAP
E7
42
42
24
24
18
08
10
10
78
ENDCHAR
STARTCHAR z
ENCODING 122
SWIDTH 480 0
DWIDTH 7 0
BBX 5 7 0 0
BITMAP
F8
88
10
20
40
88
F8
ENDCHAR
STARTCHAR braceleft
ENCODING 123
SWIDTH 617 0
DWIDTH 9 0
BBX 5 12 1 -2
BITMAP
18
20
20
20
20
C0
20
20
20
20
20
18
ENDCHAR
STARTCHAR bar
ENCODING 124
SWIDTH 342 0
DWIDTH 5 0
BBX 1 11 1 -1
BITMAP
80
80
80
80
80
80
80
80
80
80
80
ENDCHAR
STARTCHAR braceright
ENCODING 125
SWIDTH 617 0
DWIDTH 9 0
BBX 5 12 1 -2
BITMAP
C0
20
20
20
20
18
20
20
20
20
20
C0
ENDCHAR
STARTCHAR asciitilde
ENCODING 126
SWIDTH 685 0
DWIDTH 10 0
BBX 6 2 1 3
BITMAP
64
98
ENDCHAR
STARTCHAR subseteq
ENCODING 128
SWIDTH 822 0
DWIDTH 12 0
BBX 8 8 1 0
BITMAP
7F
C0
80
80
C0
7F
00
FF
ENDCHAR
STARTCHAR ransub
ENCODING 129
SWIDTH 617 0
DWIDTH 9 0
BBX 5 9 1 0
BITMAP
80
C0
A0
90
F8
90
A0
C0
80
ENDCHAR
STARTCHAR uplus
ENCODING 130
SWIDTH 754 0
DWIDTH 11 0
BBX 7 7 1 0
BITMAP
92
92
FE
92
92
C6
7C
ENDCHAR
STARTCHAR universe
ENCODING 131
SWIDTH 754 0
DWIDTH 11 0
BBX 9 10 0 0
BITMAP
FB80
5100
5100
5100
5100
5100
5100
5100
3200
1C00
ENDCHAR
STARTCHAR Delta
ENCODING 132
SWIDTH 617 0
DWIDTH 9 0
BBX 7 10 0 0
BITMAP
10
10
28
28
28
44
44
44
82
FE
ENDCHAR
STARTCHAR circ
ENCODING 133
SWIDTH 617 0
DWIDTH 9 0
BBX 5 5 1 2
BITMAP
70
88
88
88
70
ENDCHAR
STARTCHAR Phi
ENCODING 134
SWIDTH 617 0
DWIDTH 9 0
BBX 7 10 0 0
BITMAP
7C
10
38
54
92
92
54
38
10
7C
ENDCHAR
STARTCHAR Gamma
ENCODING 135
SWIDTH 617 0
DWIDTH 9 0
BBX 7 10 0 0
BITMAP
FE
46
42
42
40
40
40
40
40
E0
ENDCHAR
STARTCHAR <unkown>
ENCODING 136
SWIDTH 685 0
DWIDTH 10 0
BBX 6 8 3 4
BITMAP
C0
C0
C0
C0
C0
C0
FC
FC
ENDCHAR
STARTCHAR subscript
ENCODING 137
SWIDTH 617 0
DWIDTH 9 0
BBX 7 7 0 -2
BITMAP
82
44
28
28
38
10
10
ENDCHAR
STARTCHAR Theta
ENCODING 138
SWIDTH 685 0
DWIDTH 10 0
BBX 8 10 0 0
BITMAP
3C
42
C3
A5
BD
A5
81
C3
42
3C
ENDCHAR
STARTCHAR dcat
ENCODING 139
SWIDTH 891 0
DWIDTH 13 0
BBX 9 10 1 0
BITMAP
1080
6C80
8300
0100
0200
0200
0400
0400
0800
0800
ENDCHAR
STARTCHAR Lambda
ENCODING 140
SWIDTH 754 0
DWIDTH 11 0
BBX 9 9 0 0
BITMAP
0800
0800
1400
1400
2200
2200
4100
4100
E380
ENDCHAR
STARTCHAR in
ENCODING 141
SWIDTH 754 0
DWIDTH 11 0
BBX 7 7 1 0
BITMAP
3E
40
80
FE
80
40
3E
ENDCHAR
STARTCHAR notin
ENCODING 142
SWIDTH 754 0
DWIDTH 11 0
BBX 7 11 1 -2
BITMAP
04
04
3E
48
88
FE
90
50
3E
20
20
ENDCHAR
STARTCHAR bij
ENCODING 143
SWIDTH 891 0
DWIDTH 13 0
BBX 11 5 0 2
BITMAP
8480
4240
7FE0
4240
8480
ENDCHAR
STARTCHAR Pi
ENCODING 144
SWIDTH 685 0
DWIDTH 10 0
BBX 8 10 0 0
BITMAP
FF
42
42
42
42
42
42
42
42
E7
ENDCHAR
STARTCHAR mlquote
ENCODING 145
SWIDTH 754 0
DWIDTH 11 0
BBX 9 13 0 -2
BITMAP
FF00
8000
8000
8000
8000
8000
0000
8A00
DA00
AA00
8A00
8A00
8B80
ENDCHAR
STARTCHAR ranres
ENCODING 146
SWIDTH 617 0
DWIDTH 9 0
BBX 5 9 1 0
BITMAP
80
C0
A0
90
88
90
A0
C0
80
ENDCHAR
STARTCHAR Sigma
ENCODING 147
SWIDTH 617 0
DWIDTH 9 0
BBX 7 10 0 0
BITMAP
FE
82
40
20
10
10
20
40
82
FE
ENDCHAR
STARTCHAR typequote
ENCODING 148
SWIDTH 685 0
DWIDTH 10 0
BBX 8 7 0 4
BITMAP
FF
80
83
83
80
83
83
ENDCHAR
STARTCHAR Upsilon
ENCODING 149
SWIDTH 754 0
DWIDTH 11 0
BBX 9 10 0 0
BITMAP
6300
9480
0800
0800
0800
0800
0800
0800
0800
3E00
ENDCHAR
STARTCHAR bool
ENCODING 150
SWIDTH 685 0
DWIDTH 10 0
BBX 8 10 0 0
BITMAP
FC
52
52
56
5C
52
51
51
53
FE
ENDCHAR
STARTCHAR Omega
ENCODING 151
SWIDTH 754 0
DWIDTH 11 0
BBX 9 10 0 0
BITMAP
1C00
2200
4100
4100
4100
4100
2200
2200
9480
7700
ENDCHAR
STARTCHAR Xi
ENCODING 152
SWIDTH 617 0
DWIDTH 9 0
BBX 7 9 0 0
BITMAP
FE
82
00
44
7C
44
00
82
FE
ENDCHAR
STARTCHAR Psi
ENCODING 153
SWIDTH 754 0
DWIDTH 11 0
BBX 9 10 0 0
BITMAP
3E00
0800
C980
4900
4900
6B00
3E00
0800
0800
3E00
ENDCHAR
STARTCHAR emptyset
ENCODING 154
SWIDTH 754 0
DWIDTH 11 0
BBX 7 7 1 1
BITMAP
3A
44
8A
92
A2
44
B8
ENDCHAR
STARTCHAR superscript
ENCODING 155
SWIDTH 617 0
DWIDTH 9 0
BBX 7 7 0 4
BITMAP
10
10
38
28
28
44
82
ENDCHAR
STARTCHAR <unkown>
ENCODING 156
SWIDTH 685 0
DWIDTH 10 0
BBX 10 6 -1 1
BITMAP
FFC0
FFC0
0000
0000
FFC0
FFC0
ENDCHAR
STARTCHAR <unkown>
ENCODING 157
SWIDTH 685 0
DWIDTH 10 0
BBX 6 10 3 -3
BITMAP
FC
FC
C0
C0
FC
FC
C0
C0
C0
C0
ENDCHAR
STARTCHAR finj
ENCODING 158
SWIDTH 960 0
DWIDTH 14 0
BBX 12 5 0 2
BITMAP
8A40
4A20
7FF0
4A20
8A40
ENDCHAR
STARTCHAR finj
ENCODING 159
SWIDTH 960 0
DWIDTH 14 0
BBX 12 5 0 2
BITMAP
0A40
0A20
FFF0
0A20
0A40
ENDCHAR
STARTCHAR subset
ENCODING 160
SWIDTH 822 0
DWIDTH 12 0
BBX 8 6 1 2
BITMAP
7F
C0
80
80
C0
7F
ENDCHAR
STARTCHAR cap
ENCODING 161
SWIDTH 754 0
DWIDTH 11 0
BBX 7 7 1 0
BITMAP
7C
C6
82
82
82
82
82
ENDCHAR
STARTCHAR rangle
ENCODING 162
SWIDTH 548 0
DWIDTH 8 0
BBX 4 13 1 -2
BITMAP
80
80
40
40
20
20
10
20
20
40
40
80
80
ENDCHAR
STARTCHAR ominus
ENCODING 163
SWIDTH 754 0
DWIDTH 11 0
BBX 7 7 1 1
BITMAP
38
44
82
FE
82
44
38
ENDCHAR
STARTCHAR iff
ENCODING 164
SWIDTH 1097 0
DWIDTH 16 0
BBX 12 7 1 0
BITMAP
1080
2040
7FE0
C030
7FE0
2040
1080
ENDCHAR
STARTCHAR bigcap
ENCODING 165
SWIDTH 891 0
DWIDTH 13 0
BBX 9 10 1 0
BITMAP
3E00
7F00
E380
C180
C180
C180
C180
C180
C180
C180
ENDCHAR
STARTCHAR defs
ENCODING 166
SWIDTH 754 0
DWIDTH 11 0
BBX 7 7 1 1
BITMAP
10
28
44
00
FE
00
FE
ENDCHAR
STARTCHAR langle
ENCODING 167
SWIDTH 548 0
DWIDTH 8 0
BBX 4 13 1 -2
BITMAP
10
10
20
20
40
40
80
40
40
20
20
10
10
ENDCHAR
STARTCHAR limg
ENCODING 168
SWIDTH 548 0
DWIDTH 8 0
BBX 4 12 1 -2
BITMAP
10
20
60
A0
A0
A0
A0
A0
A0
60
20
10
ENDCHAR
STARTCHAR rimg
ENCODING 169
SWIDTH 548 0
DWIDTH 8 0
BBX 4 12 1 -2
BITMAP
80
40
60
50
50
50
50
50
50
60
40
80
ENDCHAR
STARTCHAR rel
ENCODING 170
SWIDTH 822 0
DWIDTH 12 0
BBX 10 5 0 2
BITMAP
2100
4080
FFC0
4080
2100
ENDCHAR
STARTCHAR oplus
ENCODING 171
SWIDTH 754 0
DWIDTH 11 0
BBX 7 7 1 1
BITMAP
38
54
92
FE
92
54
38
ENDCHAR
STARTCHAR openquote
ENCODING 172
SWIDTH 685 0
DWIDTH 10 0
BBX 8 6 0 5
BITMAP
FF
80
80
80
80
80
ENDCHAR
STARTCHAR fun
ENCODING 173
SWIDTH 822 0
DWIDTH 12 0
BBX 10 5 0 2
BITMAP
0100
0080
FFC0
0080
0100
ENDCHAR
STARTCHAR closequote
ENCODING 174
SWIDTH 685 0
DWIDTH 10 0
BBX 8 6 0 5
BITMAP
FF
01
01
01
01
01
ENDCHAR
STARTCHAR real
ENCODING 175
SWIDTH 754 0
DWIDTH 11 0
BBX 9 10 0 0
BITMAP
FE00
5300
5100
5100
5200
5C00
5200
5200
5100
FB80
ENDCHAR
STARTCHAR <unknown>
ENCODING 176
SWIDTH 685 0
DWIDTH 10 0
BBX 8 8 0 3
BITMAP
FF
FF
FF
FF
FF
FF
FF
FF
ENDCHAR
STARTCHAR and
ENCODING 177
SWIDTH 754 0
DWIDTH 11 0
BBX 7 8 1 0
BITMAP
10
10
28
28
44
44
82
82
ENDCHAR
STARTCHAR or
ENCODING 178
SWIDTH 754 0
DWIDTH 11 0
BBX 7 8 1 0
BITMAP
82
82
44
44
28
28
10
10
ENDCHAR
STARTCHAR not
ENCODING 179
SWIDTH 754 0
DWIDTH 11 0
BBX 7 4 1 2
BITMAP
FE
02
02
02
ENDCHAR
STARTCHAR implies
ENCODING 180
SWIDTH 960 0
DWIDTH 14 0
BBX 10 7 1 0
BITMAP
0200
0100
FF80
00C0
FF80
0100
0200
ENDCHAR
STARTCHAR forall
ENCODING 181
SWIDTH 891 0
DWIDTH 13 0
BBX 9 10 1 0
BITMAP
E380
4100
4100
2200
3E00
2200
1400
1400
0800
0800
ENDCHAR
STARTCHAR exists
ENCODING 182
SWIDTH 754 0
DWIDTH 11 0
BBX 7 10 1 0
BITMAP
FE
84
04
24
3C
24
04
04
84
FE
ENDCHAR
STARTCHAR dot
ENCODING 183
SWIDTH 617 0
DWIDTH 9 0
BBX 5 5 1 2
BITMAP
70
F8
F8
F8
70
ENDCHAR
STARTCHAR times
ENCODING 184
SWIDTH 754 0
DWIDTH 11 0
BBX 7 7 1 1
BITMAP
82
44
28
10
28
44
82
ENDCHAR
STARTCHAR S
ENCODING 185
SWIDTH 685 0
DWIDTH 10 0
BBX 8 14 0 -2
BITMAP
3C
42
99
A5
A5
A5
91
89
A5
A5
A5
99
42
3C
ENDCHAR
STARTCHAR typecolon
ENCODING 186
SWIDTH 617 0
DWIDTH 9 0
BBX 5 11 1 -1
BITMAP
70
A8
F8
A8
70
00
70
A8
F8
A8
70
ENDCHAR
STARTCHAR comp
ENCODING 187
SWIDTH 548 0
DWIDTH 8 0
BBX 4 11 1 -2
BITMAP
60
90
90
60
00
60
90
90
70
20
40
ENDCHAR
STARTCHAR leq
ENCODING 188
SWIDTH 754 0
DWIDTH 11 0
BBX 7 10 1 -1
BITMAP
06
18
60
80
60
18
86
60
18
06
ENDCHAR
STARTCHAR notequal
ENCODING 189
SWIDTH 754 0
DWIDTH 11 0
BBX 7 7 1 1
BITMAP
08
08
FE
10
FE
20
20
ENDCHAR
STARTCHAR geq
ENCODING 190
SWIDTH 754 0
DWIDTH 11 0
BBX 7 10 1 -1
BITMAP
C0
30
0C
02
0C
30
C2
0C
30
C0
ENDCHAR
STARTCHAR string
ENCODING 191
SWIDTH 617 0
DWIDTH 9 0
BBX 7 10 0 0
BITMAP
7A
D6
A2
B0
48
34
0A
8A
D6
BC
ENDCHAR
STARTCHAR cup
ENCODING 192
SWIDTH 754 0
DWIDTH 11 0
BBX 7 7 1 0
BITMAP
82
82
82
82
82
C6
7C
ENDCHAR
STARTCHAR alpha
ENCODING 193
SWIDTH 685 0
DWIDTH 10 0
BBX 8 6 0 0
BITMAP
32
4A
8A
84
8D
73
ENDCHAR
STARTCHAR beta
ENCODING 194
SWIDTH 548 0
DWIDTH 8 0
BBX 6 12 0 -2
BITMAP
30
48
88
88
90
B8
84
84
C4
B8
80
80
ENDCHAR
STARTCHAR refinement
ENCODING 195
SWIDTH 822 0
DWIDTH 12 0
BBX 8 8 1 1
BITMAP
FF
80
80
80
FF
00
00
FF
ENDCHAR
STARTCHAR delta
ENCODING 196
SWIDTH 480 0
DWIDTH 7 0
BBX 5 10 0 0
BITMAP
70
88
80
40
20
50
88
88
88
70
ENDCHAR
STARTCHAR epsilon
ENCODING 197
SWIDTH 548 0
DWIDTH 8 0
BBX 6 7 0 0
BITMAP
70
88
80
60
80
84
78
ENDCHAR
STARTCHAR <unknown>
ENCODING 198
SWIDTH 617 0
DWIDTH 9 0
BBX 7 12 0 -2
BITMAP
10
10
10
38
54
92
92
92
54
38
10
10
ENDCHAR
STARTCHAR gamma
ENCODING 199
SWIDTH 685 0
DWIDTH 10 0
BBX 8 9 0 -2
BITMAP
71
C9
85
06
02
02
02
02
02
ENDCHAR
STARTCHAR eta
ENCODING 200
SWIDTH 548 0
DWIDTH 8 0
BBX 6 8 0 -2
BITMAP
D8
A4
A4
24
24
24
04
04
ENDCHAR
STARTCHAR iota
ENCODING 201
SWIDTH 411 0
DWIDTH 6 0
BBX 4 6 0 0
BITMAP
C0
40
40
50
50
60
ENDCHAR
STARTCHAR theta
ENCODING 202
SWIDTH 548 0
DWIDTH 8 0
BBX 6 10 0 0
BITMAP
30
48
84
84
FC
84
84
84
48
30
ENDCHAR
STARTCHAR kappa
ENCODING 203
SWIDTH 548 0
DWIDTH 8 0
BBX 6 6 0 0
BITMAP
8C
90
E0
B0
88
84
ENDCHAR
STARTCHAR lambda
ENCODING 204
SWIDTH 685 0
DWIDTH 10 0
BBX 8 10 0 0
BITMAP
C0
20
20
10
10
18
28
44
45
82
ENDCHAR
STARTCHAR mu
ENCODING 205
SWIDTH 617 0
DWIDTH 9 0
BBX 7 8 0 -2
BITMAP
88
88
88
88
9A
F6
80
80
ENDCHAR
STARTCHAR nu
ENCODING 206
SWIDTH 548 0
DWIDTH 8 0
BBX 6 6 0 0
BITMAP
C4
44
44
48
50
60
ENDCHAR
STARTCHAR psurj
ENCODING 207
SWIDTH 891 0
DWIDTH 13 0
BBX 11 5 0 2
BITMAP
2480
2240
FFE0
2240
2480
ENDCHAR
STARTCHAR pi
ENCODING 208
SWIDTH 685 0
DWIDTH 10 0
BBX 8 7 0 0
BITMAP
7F
94
14
14
14
14
22
ENDCHAR
STARTCHAR Xi
ENCODING 209
SWIDTH 685 0
DWIDTH 10 0
BBX 8 10 0 -2
BITMAP
C2
A2
24
14
18
18
28
24
44
43
ENDCHAR
STARTCHAR rho
ENCODING 210
SWIDTH 548 0
DWIDTH 8 0
BBX 6 9 0 -2
BITMAP
30
48
84
84
84
C8
B0
80
80
ENDCHAR
STARTCHAR sigma
ENCODING 211
SWIDTH 617 0
DWIDTH 9 0
BBX 7 7 0 0
BITMAP
3E
48
84
84
84
48
30
ENDCHAR
STARTCHAR tau
ENCODING 212
SWIDTH 617 0
DWIDTH 9 0
BBX 7 7 0 0
BITMAP
7E
90
10
10
10
14
08
ENDCHAR
STARTCHAR nu
ENCODING 213
SWIDTH 685 0
DWIDTH 10 0
BBX 8 6 0 0
BITMAP
62
A1
21
21
22
1C
ENDCHAR
STARTCHAR complex
ENCODING 214
SWIDTH 685 0
DWIDTH 10 0
BBX 8 10 0 0
BITMAP
3D
53
A1
A0
A0
A0
A0
A1
D3
7E
ENDCHAR
STARTCHAR omega
ENCODING 215
SWIDTH 754 0
DWIDTH 11 0
BBX 9 6 0 0
BITMAP
6300
8080
8880
8880
4C80
3300
ENDCHAR
STARTCHAR xi
ENCODING 216
SWIDTH 480 0
DWIDTH 7 0
BBX 6 12 0 -2
BITMAP
58
30
40
80
88
70
20
40
40
38
04
18
ENDCHAR
STARTCHAR <unknown>
ENCODING 217
SWIDTH 754 0
DWIDTH 11 0
BBX 9 12 0 -2
BITMAP
0400
0400
0400
4500
A480
A480
2480
2480
1500
0E00
0400
0400
ENDCHAR
STARTCHAR zeta
ENCODING 218
SWIDTH 480 0
DWIDTH 7 0
BBX 5 12 0 -2
BITMAP
58
38
20
40
80
80
80
40
30
08
08
70
ENDCHAR
STARTCHAR idxopen
ENCODING 219
SWIDTH 685 0
DWIDTH 10 0
BBX 8 13 0 -3
BITMAP
E0
80
80
80
80
80
80
80
91
8A
E4
0A
11
ENDCHAR
STARTCHAR <unknown>
ENCODING 220
SWIDTH 685 0
DWIDTH 10 0
BBX 2 15 3 -3
BITMAP
C0
C0
C0
C0
C0
C0
C0
C0
C0
C0
C0
C0
C0
C0
C0
ENDCHAR
STARTCHAR idxclose
ENCODING 221
SWIDTH 685 0
DWIDTH 10 0
BBX 8 13 0 -3
BITMAP
07
01
01
01
01
01
01
01
89
51
27
50
88
ENDCHAR
STARTCHAR bigcup
ENCODING 222
SWIDTH 891 0
DWIDTH 13 0
BBX 9 10 1 0
BITMAP
C180
C180
C180
C180
C180
C180
C180
E380
7F00
3E00
ENDCHAR
STARTCHAR pfun
ENCODING 223
SWIDTH 891 0
DWIDTH 13 0
BBX 11 5 0 2
BITMAP
0480
0440
FFE0
0440
0480
ENDCHAR
STARTCHAR inj
ENCODING 224
SWIDTH 891 0
DWIDTH 13 0
BBX 11 5 0 2
BITMAP
8080
4040
7FE0
4040
8080
ENDCHAR
STARTCHAR domsub
ENCODING 225
SWIDTH 617 0
DWIDTH 9 0
BBX 5 9 1 0
BITMAP
08
18
28
48
F8
48
28
18
08
ENDCHAR
STARTCHAR bottom
ENCODING 226
SWIDTH 754 0
DWIDTH 11 0
BBX 7 8 1 0
BITMAP
10
10
10
10
10
10
10
FE
ENDCHAR
STARTCHAR limplies
ENCODING 227
SWIDTH 960 0
DWIDTH 14 0
BBX 10 7 1 0
BITMAP
1000
2000
7FC0
C000
7FC0
2000
1000
ENDCHAR
STARTCHAR rsubset
ENCODING 228
SWIDTH 822 0
DWIDTH 12 0
BBX 8 6 1 2
BITMAP
FE
03
01
01
03
FE
ENDCHAR
STARTCHAR rsubseteq
ENCODING 229
SWIDTH 822 0
DWIDTH 12 0
BBX 8 8 1 0
BITMAP
FE
03
01
01
03
FE
00
FF
ENDCHAR
STARTCHAR finset
ENCODING 230
SWIDTH 822 0
DWIDTH 12 0
BBX 8 10 1 0
BITMAP
FF
51
50
50
5E
50
50
50
50
F8
ENDCHAR
STARTCHAR uprightarrow
ENCODING 231
SWIDTH 617 0
DWIDTH 9 0
BBX 7 7 0 2
BITMAP
3E
06
0A
12
22
40
80
ENDCHAR
STARTCHAR downrightarrow
ENCODING 232
SWIDTH 617 0
DWIDTH 9 0
BBX 7 7 0 0
BITMAP
80
40
22
12
0A
06
3E
ENDCHAR
STARTCHAR equiv
ENCODING 233
SWIDTH 822 0
DWIDTH 12 0
BBX 8 5 1 2
BITMAP
FF
00
FF
00
FF
ENDCHAR
STARTCHAR updownarrow
ENCODING 234
SWIDTH 480 0
DWIDTH 7 0
BBX 5 10 0 0
BITMAP
20
70
A8
20
20
20
20
A8
70
20
ENDCHAR
STARTCHAR cat
ENCODING 235
SWIDTH 754 0
DWIDTH 11 0
BBX 7 3 1 7
BITMAP
10
6C
82
ENDCHAR
STARTCHAR extract
ENCODING 236
SWIDTH 480 0
DWIDTH 7 0
BBX 3 10 1 0
BITMAP
20
20
60
60
A0
20
20
20
20
20
ENDCHAR
STARTCHAR maplet
ENCODING 237
SWIDTH 891 0
DWIDTH 13 0
BBX 9 5 1 2
BITMAP
8200
8100
FF80
8100
8200
ENDCHAR
STARTCHAR nat
ENCODING 238
SWIDTH 685 0
DWIDTH 10 0
BBX 8 10 0 0
BITMAP
E7
52
52
6A
6A
56
56
4A
4A
E7
ENDCHAR
STARTCHAR surj
ENCODING 239
SWIDTH 891 0
DWIDTH 13 0
BBX 11 5 0 2
BITMAP
0480
0240
FFE0
0240
0480
ENDCHAR
STARTCHAR power
ENCODING 240
SWIDTH 822 0
DWIDTH 12 0
BBX 8 10 1 0
BITMAP
FE
53
51
51
52
5C
50
50
50
F8
ENDCHAR
STARTCHAR zquote
ENCODING 241
SWIDTH 685 0
DWIDTH 10 0
BBX 8 13 0 -2
BITMAP
FF
80
80
80
80
80
00
7E
44
08
10
22
7E
ENDCHAR
STARTCHAR domres
ENCODING 242
SWIDTH 617 0
DWIDTH 9 0
BBX 5 9 1 0
BITMAP
08
18
28
48
88
48
28
18
08
ENDCHAR
STARTCHAR rat
ENCODING 243
SWIDTH 685 0
DWIDTH 10 0
BBX 8 12 0 -2
BITMAP
3E
43
A1
A1
A1
A1
A1
A1
D2
7C
61
BE
ENDCHAR
STARTCHAR vdash
ENCODING 244
SWIDTH 754 0
DWIDTH 11 0
BBX 7 7 1 1
BITMAP
80
80
80
FE
80
80
80
ENDCHAR
STARTCHAR free
ENCODING 245
SWIDTH 754 0
DWIDTH 11 0
BBX 9 12 0 -1
BITMAP
7F00
C180
9C80
A280
A280
8480
8880
8880
8080
8880
C180
7F00
ENDCHAR
STARTCHAR free
ENCODING 246
SWIDTH 754 0
DWIDTH 11 0
BBX 9 12 0 -1
BITMAP
7F00
C180
9C80
A280
A280
8480
8880
8880
8080
8880
C180
7F00
ENDCHAR
STARTCHAR <unknown>
ENCODING 247
SWIDTH 685 0
DWIDTH 10 0
BBX 6 15 3 -3
BITMAP
C0
C0
C0
C0
C0
C0
FC
FC
C0
C0
C0
C0
C0
C0
C0
ENDCHAR
STARTCHAR free
ENCODING 248
SWIDTH 754 0
DWIDTH 11 0
BBX 9 12 0 -1
BITMAP
7F00
C180
9C80
A280
A280
8480
8880
8880
8080
8880
C180
7F00
ENDCHAR
STARTCHAR filter
ENCODING 249
SWIDTH 480 0
DWIDTH 7 0
BBX 3 10 1 0
BITMAP
80
80
C0
C0
A0
80
80
80
80
80
ENDCHAR
STARTCHAR num
ENCODING 250
SWIDTH 548 0
DWIDTH 8 0
BBX 6 10 0 0
BITMAP
FC
94
94
28
28
50
50
A4
A4
FC
ENDCHAR
STARTCHAR lrect
ENCODING 251
SWIDTH 548 0
DWIDTH 8 0
BBX 5 12 1 -2
BITMAP
F8
A0
A0
A0
A0
A0
A0
A0
A0
A0
A0
F8
ENDCHAR
STARTCHAR <unknown>
ENCODING 252
SWIDTH 685 0
DWIDTH 10 0
BBX 10 2 -1 4
BITMAP
FFC0
FFC0
ENDCHAR
STARTCHAR rrect
ENCODING 253
SWIDTH 548 0
DWIDTH 8 0
BBX 5 12 0 -2
BITMAP
F8
28
28
28
28
28
28
28
28
28
28
F8
ENDCHAR
STARTCHAR pinf
ENCODING 254
SWIDTH 891 0
DWIDTH 13 0
BBX 11 5 0 2
BITMAP
8480
4440
7FE0
4440
8480
ENDCHAR
STARTCHAR <unkown>
ENCODING 255
SWIDTH 685 0
DWIDTH 10 0
BBX 6 10 3 -3
BITMAP
FC
FC
C0
C0
C0
C0
C0
C0
C0
C0
ENDCHAR
ENDFONT
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
