# HG changeset patch
# User wenzelm
# Date 857741460 -3600
# Node ID f433eb78b927721a4fa26e3fe48e5f68a639df39
# Parent  3090e4a1a3178a4ee105453ff34744517d88a590
now sans serifs;

diff -r 3090e4a1a317 -r f433eb78b927 lib/fonts/isabelle14.bdf
--- 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