--- a/lib/fonts/isabelle14.bdf Fri Mar 07 13:47:37 1997 +0100
+++ b/lib/fonts/isabelle14.bdf Fri Mar 07 14:31:00 1997 +0100
@@ -87,14 +87,14 @@
BITMAP
20
20
-78
+70
88
80
-c0
+40
30
08
88
-f0
+70
20
20
20
@@ -274,7 +274,7 @@
ENCODING 49
SWIDTH 600 0
DWIDTH 9 0
-BBX 5 10 1 0
+BBX 4 10 1 0
BITMAP
20
60
@@ -285,7 +285,7 @@
20
20
20
-f8
+70
ENDCHAR
STARTCHAR two
ENCODING 50
@@ -301,7 +301,7 @@
10
20
40
-84
+80
fc
ENDCHAR
STARTCHAR three
@@ -336,7 +336,7 @@
88
fc
08
-1c
+08
ENDCHAR
STARTCHAR five
ENCODING 53
@@ -511,7 +511,7 @@
ENCODING 64
SWIDTH 600 0
DWIDTH 9 0
-BBX 7 10 1 -1
+BBX 6 10 1 -1
BITMAP
38
44
@@ -519,7 +519,7 @@
9c
a4
a4
-9e
+9c
80
40
38
@@ -528,33 +528,33 @@
ENCODING 65
SWIDTH 600 0
DWIDTH 9 0
-BBX 9 9 0 0
+BBX 7 9 1 0
BITMAP
-3800
-0800
-1400
-1400
-2200
-3e00
-4100
-4100
-f780
+10
+10
+28
+28
+44
+7c
+82
+82
+82
ENDCHAR
STARTCHAR B
ENCODING 66
SWIDTH 600 0
DWIDTH 9 0
-BBX 7 9 1 0
+BBX 6 9 1 0
BITMAP
-fc
-42
-42
-42
-7c
-42
-42
-42
-fc
+f8
+84
+84
+84
+f8
+84
+84
+84
+f8
ENDCHAR
STARTCHAR C
ENCODING 67
@@ -562,9 +562,9 @@
DWIDTH 9 0
BBX 7 9 1 0
BITMAP
-3a
-46
-82
+3c
+42
+80
80
80
80
@@ -576,62 +576,62 @@
ENCODING 68
SWIDTH 600 0
DWIDTH 9 0
-BBX 8 9 0 0
+BBX 7 9 1 0
BITMAP
-fc
-42
-41
-41
-41
-41
-41
-42
-fc
+f8
+84
+82
+82
+82
+82
+82
+84
+f8
ENDCHAR
STARTCHAR E
ENCODING 69
SWIDTH 600 0
DWIDTH 9 0
-BBX 7 9 1 0
+BBX 6 9 1 0
BITMAP
-fe
-42
-42
-48
-78
-48
-42
-42
-fe
+fc
+80
+80
+80
+f0
+80
+80
+80
+fc
ENDCHAR
STARTCHAR F
ENCODING 70
SWIDTH 600 0
DWIDTH 9 0
-BBX 7 9 1 0
+BBX 6 9 1 0
BITMAP
-fe
-42
-42
-48
-78
-48
-40
-40
+fc
+80
+80
+80
f0
+80
+80
+80
+80
ENDCHAR
STARTCHAR G
ENCODING 71
SWIDTH 600 0
DWIDTH 9 0
-BBX 8 9 0 0
+BBX 7 9 0 0
BITMAP
-3a
-46
-82
+3c
+42
80
80
-8f
+80
+8e
82
42
3c
@@ -640,41 +640,41 @@
ENCODING 72
SWIDTH 600 0
DWIDTH 9 0
-BBX 8 9 0 0
+BBX 6 9 1 0
BITMAP
-e7
-42
-42
-42
-7e
-42
-42
-42
-e7
+84
+84
+84
+84
+fc
+84
+84
+84
+84
ENDCHAR
STARTCHAR I
ENCODING 73
SWIDTH 600 0
DWIDTH 9 0
-BBX 5 9 2 0
+BBX 3 9 2 0
BITMAP
-f8
-20
-20
-20
-20
-20
-20
-20
-f8
+e0
+40
+40
+40
+40
+40
+40
+40
+e0
ENDCHAR
STARTCHAR J
ENCODING 74
SWIDTH 600 0
DWIDTH 9 0
-BBX 7 9 1 0
+BBX 6 9 1 0
BITMAP
-3e
+1c
08
08
08
@@ -688,65 +688,65 @@
ENCODING 75
SWIDTH 600 0
DWIDTH 9 0
-BBX 8 9 0 0
+BBX 6 9 1 0
BITMAP
-ee
-44
-48
-50
-70
-48
-44
-44
-e3
+84
+88
+90
+a0
+e0
+90
+88
+88
+84
ENDCHAR
STARTCHAR L
ENCODING 76
SWIDTH 600 0
DWIDTH 9 0
-BBX 8 9 0 0
+BBX 7 9 0 0
BITMAP
-f8
-20
-20
-20
-20
-21
-21
-21
-ff
+e0
+40
+40
+40
+40
+40
+40
+42
+7e
ENDCHAR
STARTCHAR M
ENCODING 77
SWIDTH 600 0
DWIDTH 9 0
-BBX 9 9 0 0
+BBX 7 9 1 0
BITMAP
-e380
-6300
-5700
-5500
-4900
-4900
-4100
-4100
-e380
+c6
+c6
+aa
+aa
+92
+92
+82
+82
+82
ENDCHAR
STARTCHAR N
ENCODING 78
SWIDTH 600 0
DWIDTH 9 0
-BBX 8 9 0 0
+BBX 6 9 1 0
BITMAP
-e7
-62
-52
-52
-4a
-4a
-46
-46
-e2
+c4
+c4
+a4
+a4
+94
+94
+8c
+8c
+84
ENDCHAR
STARTCHAR O
ENCODING 79
@@ -768,17 +768,17 @@
ENCODING 80
SWIDTH 600 0
DWIDTH 9 0
-BBX 7 9 1 0
+BBX 6 9 1 0
BITMAP
-fc
-42
-42
-42
-42
-7c
-40
-40
-f0
+f8
+84
+84
+84
+84
+f8
+80
+80
+80
ENDCHAR
STARTCHAR Q
ENCODING 81
@@ -802,17 +802,17 @@
ENCODING 82
SWIDTH 600 0
DWIDTH 9 0
-BBX 8 9 0 0
+BBX 7 9 1 0
BITMAP
-fc
-42
-42
-42
-44
-78
-44
-42
-e1
+f8
+84
+84
+84
+88
+f0
+88
+84
+82
ENDCHAR
STARTCHAR S
ENCODING 83
@@ -820,15 +820,15 @@
DWIDTH 9 0
BBX 6 9 1 0
BITMAP
-74
-8c
+78
84
80
+80
78
04
+04
84
-c4
-b8
+78
ENDCHAR
STARTCHAR T
ENCODING 84
@@ -837,62 +837,62 @@
BBX 7 9 1 0
BITMAP
fe
-92
-92
10
10
10
10
10
-7c
+10
+10
+10
ENDCHAR
STARTCHAR U
ENCODING 85
SWIDTH 600 0
DWIDTH 9 0
-BBX 8 9 0 0
+BBX 6 9 1 0
BITMAP
-e7
-42
-42
-42
-42
-42
-42
-42
-3c
+84
+84
+84
+84
+84
+84
+84
+84
+78
ENDCHAR
STARTCHAR V
ENCODING 86
SWIDTH 600 0
DWIDTH 9 0
-BBX 9 9 0 0
+BBX 7 9 1 0
BITMAP
-e380
-4100
-4100
-2200
-2200
-1400
-1400
-0800
-0800
+82
+82
+82
+44
+44
+28
+28
+10
+10
ENDCHAR
STARTCHAR W
ENCODING 87
SWIDTH 600 0
DWIDTH 9 0
-BBX 9 9 0 0
+BBX 7 9 1 0
BITMAP
-e380
-4100
-4900
-4900
-5500
-5500
-2200
-2200
-2200
+82
+82
+92
+92
+aa
+aa
+44
+44
+44
ENDCHAR
STARTCHAR X
ENCODING 88
@@ -900,7 +900,7 @@
DWIDTH 9 0
BBX 8 9 0 0
BITMAP
-e7
+81
42
24
24
@@ -908,7 +908,7 @@
24
24
42
-e7
+81
ENDCHAR
STARTCHAR Y
ENCODING 89
@@ -916,7 +916,7 @@
DWIDTH 9 0
BBX 7 9 1 0
BITMAP
-ee
+82
44
44
28
@@ -924,7 +924,7 @@
10
10
10
-7c
+10
ENDCHAR
STARTCHAR Z
ENCODING 90
@@ -933,13 +933,13 @@
BBX 6 9 1 0
BITMAP
fc
-84
-88
+04
+08
10
20
20
-44
-84
+40
+80
fc
ENDCHAR
STARTCHAR bracketleft
@@ -1036,7 +1036,7 @@
BBX 7 7 1 0
BITMAP
78
-84
+04
04
7c
84
@@ -1047,18 +1047,18 @@
ENCODING 98
SWIDTH 600 0
DWIDTH 9 0
-BBX 8 10 0 0
+BBX 7 10 1 0
BITMAP
-c0
-40
-40
-5c
-62
-41
-41
-41
-62
-dc
+80
+80
+80
+b8
+c4
+82
+82
+82
+c4
+b8
ENDCHAR
STARTCHAR c
ENCODING 99
@@ -1066,9 +1066,9 @@
DWIDTH 9 0
BBX 7 7 1 0
BITMAP
-3a
-46
-82
+3c
+42
+80
80
80
42
@@ -1078,9 +1078,9 @@
ENCODING 100
SWIDTH 600 0
DWIDTH 9 0
-BBX 8 10 0 0
+BBX 7 10 0 0
BITMAP
-06
+02
02
02
3a
@@ -1089,7 +1089,7 @@
82
82
46
-3b
+3a
ENDCHAR
STARTCHAR e
ENCODING 101
@@ -1120,15 +1120,15 @@
20
20
20
-f8
+20
ENDCHAR
STARTCHAR g
ENCODING 103
SWIDTH 600 0
DWIDTH 9 0
-BBX 8 10 0 -3
+BBX 7 10 0 -3
BITMAP
-3b
+3a
46
82
82
@@ -1143,107 +1143,107 @@
ENCODING 104
SWIDTH 600 0
DWIDTH 9 0
-BBX 8 10 0 0
+BBX 6 10 1 0
BITMAP
-c0
-40
-40
-5c
-62
-42
-42
-42
-42
-e7
+80
+80
+80
+b8
+c4
+84
+84
+84
+84
+84
ENDCHAR
STARTCHAR i
ENCODING 105
SWIDTH 600 0
DWIDTH 9 0
-BBX 5 10 2 0
+BBX 3 10 3 0
BITMAP
-20
-20
+40
+40
00
+c0
+40
+40
+40
+40
+40
e0
-20
-20
-20
-20
-20
-f8
ENDCHAR
STARTCHAR j
ENCODING 106
SWIDTH 600 0
DWIDTH 9 0
-BBX 5 13 1 -3
+BBX 4 13 1 -3
BITMAP
10
10
00
-f8
-08
-08
-08
-08
-08
-08
-08
+30
+10
+10
+10
10
-e0
+10
+10
+10
+20
+c0
ENDCHAR
STARTCHAR k
ENCODING 107
SWIDTH 600 0
DWIDTH 9 0
-BBX 7 9 1 0
+BBX 5 9 1 0
BITMAP
+80
+80
+98
+90
+a0
c0
-40
-4e
-48
-50
-60
-50
-48
-ce
+a0
+90
+98
ENDCHAR
STARTCHAR l
ENCODING 108
SWIDTH 600 0
DWIDTH 9 0
-BBX 5 9 2 0
+BBX 3 9 3 0
BITMAP
+c0
+40
+40
+40
+40
+40
+40
+40
e0
-20
-20
-20
-20
-20
-20
-20
-f8
ENDCHAR
STARTCHAR m
ENCODING 109
SWIDTH 600 0
DWIDTH 9 0
-BBX 9 7 0 0
+BBX 8 7 0 0
BITMAP
-db00
-6d00
-4900
-4900
-4900
-4900
-ed80
+db
+6d
+49
+49
+49
+49
+49
ENDCHAR
STARTCHAR n
ENCODING 110
SWIDTH 600 0
DWIDTH 9 0
-BBX 8 7 0 0
+BBX 7 7 0 0
BITMAP
dc
62
@@ -1251,7 +1251,7 @@
42
42
42
-e7
+42
ENDCHAR
STARTCHAR o
ENCODING 111
@@ -1271,26 +1271,26 @@
ENCODING 112
SWIDTH 600 0
DWIDTH 9 0
-BBX 8 10 0 -3
+BBX 7 10 1 -3
BITMAP
-dc
-62
-41
-41
-41
-62
-5c
-40
-40
-f0
+b8
+c4
+82
+82
+82
+c4
+b8
+80
+80
+80
ENDCHAR
STARTCHAR q
ENCODING 113
SWIDTH 600 0
DWIDTH 9 0
-BBX 8 10 0 -3
+BBX 7 10 0 -3
BITMAP
-3b
+3a
46
82
82
@@ -1299,21 +1299,21 @@
3a
02
02
-0f
+02
ENDCHAR
STARTCHAR r
ENCODING 114
SWIDTH 600 0
DWIDTH 9 0
-BBX 7 7 1 0
+BBX 6 7 1 0
BITMAP
-cc
-52
-60
-40
-40
-40
-f0
+98
+a4
+c0
+80
+80
+80
+80
ENDCHAR
STARTCHAR s
ENCODING 115
@@ -1321,13 +1321,13 @@
DWIDTH 9 0
BBX 6 7 1 0
BITMAP
-7c
+78
84
80
78
04
84
-f8
+78
ENDCHAR
STARTCHAR t
ENCODING 116
@@ -1337,7 +1337,7 @@
BITMAP
40
40
-f8
+f0
40
40
40
@@ -1349,43 +1349,43 @@
ENCODING 117
SWIDTH 600 0
DWIDTH 9 0
-BBX 8 7 0 0
+BBX 7 7 1 0
BITMAP
-c6
-42
-42
-42
-42
-46
-3b
+84
+84
+84
+84
+84
+8c
+76
ENDCHAR
STARTCHAR v
ENCODING 118
SWIDTH 600 0
DWIDTH 9 0
-BBX 8 7 0 0
+BBX 6 7 1 0
BITMAP
-e7
-42
-42
-24
-24
-18
-18
+84
+84
+84
+48
+48
+30
+30
ENDCHAR
STARTCHAR w
ENCODING 119
SWIDTH 600 0
DWIDTH 9 0
-BBX 9 7 0 0
+BBX 7 7 1 0
BITMAP
-e380
-4100
-4900
-4900
-2a00
-3600
-3600
+82
+82
+92
+92
+54
+6c
+6c
ENDCHAR
STARTCHAR x
ENCODING 120
@@ -1393,30 +1393,30 @@
DWIDTH 9 0
BBX 7 7 1 0
BITMAP
-ee
+c6
44
28
10
28
44
-ee
+c6
ENDCHAR
STARTCHAR y
ENCODING 121
SWIDTH 600 0
DWIDTH 9 0
-BBX 8 10 0 -3
+BBX 6 10 1 -3
BITMAP
-e7
-42
-42
-24
-24
-18
-08
+84
+84
+84
+48
+48
+30
10
-10
-78
+20
+20
+60
ENDCHAR
STARTCHAR z
ENCODING 122
@@ -1425,11 +1425,11 @@
BBX 5 7 1 0
BITMAP
f8
-88
+08
10
20
40
-88
+80
f8
ENDCHAR
STARTCHAR braceleft