--- a/lib/fonts/isabelle24.bdf Tue Apr 29 16:38:16 1997 +0200
+++ b/lib/fonts/isabelle24.bdf Tue Apr 29 16:39:13 1997 +0200
@@ -26,7 +26,7 @@
CAP_HEIGHT 15
X_HEIGHT 11
ENDPROPERTIES
-CHARS 191
+CHARS 206
STARTCHAR space
ENCODING 32
SWIDTH 600 0
@@ -2020,13 +2020,327 @@
e7e0
c3c0
ENDCHAR
-STARTCHAR space
+STARTCHAR lless
+ENCODING 145
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 8 16 4 -1
+BITMAP
+01
+03
+06
+0c
+19
+33
+66
+cc
+cc
+66
+33
+19
+0c
+06
+03
+01
+ENDCHAR
+STARTCHAR unlhd
+ENCODING 146
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 14 1 -2
+BITMAP
+0060
+01e0
+07e0
+1e60
+7860
+e060
+e060
+7860
+1e60
+07e0
+01e0
+0060
+0000
+ffe0
+ENDCHAR
+STARTCHAR lhd
+ENCODING 147
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 12 1 0
+BITMAP
+0060
+01e0
+07e0
+1e60
+7860
+e060
+e060
+7860
+1e60
+07e0
+01e0
+0060
+ENDCHAR
+STARTCHAR rhd
+ENCODING 148
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 12 1 0
+BITMAP
+c000
+f000
+bc00
+8f00
+83c0
+80e0
+80e0
+83c0
+8f00
+bc00
+f000
+c000
+ENDCHAR
+STARTCHAR tturnstile
+ENCODING 149
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 14 1 0
+BITMAP
+d800
+d800
+d800
+d800
+d800
+d800
+ffe0
+ffe0
+d800
+d800
+d800
+d800
+d800
+d800
+ENDCHAR
+STARTCHAR langle
+ENCODING 150
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 5 20 4 -4
+BITMAP
+18
+18
+30
+30
+30
+60
+60
+60
+c0
+c0
+c0
+60
+60
+60
+30
+30
+30
+18
+18
+18
+ENDCHAR
+STARTCHAR rangle
+ENCODING 151
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 5 20 3 -4
+BITMAP
+c0
+c0
+60
+60
+60
+30
+30
+30
+18
+18
+18
+30
+30
+30
+60
+60
+60
+c0
+c0
+c0
+ENDCHAR
+STARTCHAR choice
+ENCODING 152
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 6 15 4 -1
+BITMAP
+fc
+cc
+cc
+cc
+cc
+cc
+cc
+cc
+cc
+cc
+cc
+cc
+cc
+cc
+fc
+ENDCHAR
+STARTCHAR top
+ENCODING 153
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 10 1 2
+BITMAP
+fff0
+fff0
+0600
+0600
+0600
+0600
+0600
+0600
+0600
+0600
+ENDCHAR
+STARTCHAR Or
+ENCODING 154
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 15 1 -1
+BITMAP
+c030
+4020
+6060
+6060
+2040
+30c0
+30c0
+1080
+1980
+1980
+0900
+0f00
+0f00
+0600
+0600
+ENDCHAR
+STARTCHAR ocdot
+ENCODING 155
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 14 1 0
+BITMAP
+0780
+1fe0
+3030
+6018
+4008
+c00c
+c30c
+c30c
+c00c
+4008
+6018
+3030
+1fe0
+0780
+ENDCHAR
+STARTCHAR iota
+ENCODING 156
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 3 8 1 0
+BITMAP
+e0
+60
+60
+60
+c0
+c0
+c0
+e0
+ENDCHAR
+STARTCHAR upsilon
+ENCODING 157
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 9 8 1 0
+BITMAP
+6300
+f180
+3180
+3180
+6100
+6300
+6200
+3c00
+ENDCHAR
+STARTCHAR Upsilon
+ENCODING 158
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 15 1 0
+BITMAP
+e0c0
+3100
+1a00
+0e00
+0600
+0600
+0600
+0600
+0600
+0600
+0600
+0600
+0600
+0600
+0f00
+ENDCHAR
+STARTCHAR Xi
+ENCODING 159
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 15 1 0
+BITMAP
+fff0
+fff0
+c030
+0000
+0000
+1080
+1f80
+1f80
+1080
+0000
+0000
+0000
+c030
+fff0
+fff0
+ENDCHAR
+STARTCHAR space2
ENCODING 160
SWIDTH 600 0
DWIDTH 15 0
-BBX 1 1 0 0
+BBX 11 2 1 0
BITMAP
-00
+8420
+ffe0
ENDCHAR
STARTCHAR Gamma
ENCODING 161
@@ -2116,7 +2430,7 @@
c060
e0f0
ENDCHAR
-STARTCHAR C167
+STARTCHAR Pi
ENCODING 165
SWIDTH 600 0
DWIDTH 15 0
@@ -2138,7 +2452,7 @@
3060
78f0
ENDCHAR
-STARTCHAR C167
+STARTCHAR Sigma
ENCODING 166
SWIDTH 600 0
DWIDTH 15 0
@@ -2160,7 +2474,7 @@
fff0
ffe0
ENDCHAR
-STARTCHAR C167
+STARTCHAR Phi
ENCODING 167
SWIDTH 600 0
DWIDTH 15 0
@@ -2181,7 +2495,7 @@
0600
0f00
ENDCHAR
-STARTCHAR C167
+STARTCHAR Psi
ENCODING 168
SWIDTH 600 0
DWIDTH 15 0
@@ -2202,7 +2516,7 @@
0600
0f00
ENDCHAR
-STARTCHAR C167
+STARTCHAR Omega
ENCODING 169
SWIDTH 600 0
DWIDTH 15 0
@@ -2223,7 +2537,7 @@
f9f0
f9f0
ENDCHAR
-STARTCHAR a
+STARTCHAR alpha
ENCODING 170
SWIDTH 600 0
DWIDTH 15 0
@@ -2240,7 +2554,7 @@
7fb8
3e18
ENDCHAR
-STARTCHAR C177
+STARTCHAR beta
ENCODING 171
SWIDTH 600 0
DWIDTH 15 0
@@ -2263,7 +2577,7 @@
c000
c000
ENDCHAR
-STARTCHAR C177
+STARTCHAR gamma
ENCODING 172
SWIDTH 600 0
DWIDTH 15 0
@@ -2283,7 +2597,7 @@
3c00
1800
ENDCHAR
-STARTCHAR C170
+STARTCHAR delta
ENCODING 173
SWIDTH 600 0
DWIDTH 15 0
@@ -2304,7 +2618,7 @@
7f00
3c00
ENDCHAR
-STARTCHAR C177
+STARTCHAR epsilon
ENCODING 174
SWIDTH 600 0
DWIDTH 15 0
@@ -2323,7 +2637,7 @@
7e
3c
ENDCHAR
-STARTCHAR C177
+STARTCHAR zeta
ENCODING 175
SWIDTH 600 0
DWIDTH 15 0
@@ -2346,7 +2660,7 @@
06
06
ENDCHAR
-STARTCHAR C177
+STARTCHAR eta
ENCODING 176
SWIDTH 600 0
DWIDTH 15 0
@@ -2365,7 +2679,7 @@
0600
0600
ENDCHAR
-STARTCHAR C177
+STARTCHAR theta
ENCODING 177
SWIDTH 600 0
DWIDTH 15 0
@@ -2384,7 +2698,7 @@
6600
3c00
ENDCHAR
-STARTCHAR C177
+STARTCHAR kappa
ENCODING 178
SWIDTH 600 0
DWIDTH 15 0
@@ -2399,7 +2713,7 @@
6680
c300
ENDCHAR
-STARTCHAR C177
+STARTCHAR lambda
ENCODING 179
SWIDTH 600 0
DWIDTH 15 0
@@ -2419,7 +2733,7 @@
4300
c180
ENDCHAR
-STARTCHAR C177
+STARTCHAR mu
ENCODING 180
SWIDTH 600 0
DWIDTH 15 0
@@ -2438,7 +2752,7 @@
c000
c000
ENDCHAR
-STARTCHAR C177
+STARTCHAR nu
ENCODING 181
SWIDTH 600 0
DWIDTH 15 0
@@ -2453,7 +2767,7 @@
7c
78
ENDCHAR
-STARTCHAR C167
+STARTCHAR xi
ENCODING 182
SWIDTH 600 0
DWIDTH 15 0
@@ -2475,7 +2789,7 @@
06
0c
ENDCHAR
-STARTCHAR C177
+STARTCHAR pi
ENCODING 183
SWIDTH 600 0
DWIDTH 15 0
@@ -2491,7 +2805,7 @@
3180
3180
ENDCHAR
-STARTCHAR C177
+STARTCHAR rho
ENCODING 184
SWIDTH 600 0
DWIDTH 15 0
@@ -2510,7 +2824,7 @@
60
c0
ENDCHAR
-STARTCHAR C167
+STARTCHAR sigma
ENCODING 185
SWIDTH 600 0
DWIDTH 15 0
@@ -2524,7 +2838,7 @@
cc00
7800
ENDCHAR
-STARTCHAR C167
+STARTCHAR tau
ENCODING 186
SWIDTH 600 0
DWIDTH 15 0
@@ -2540,7 +2854,7 @@
3200
1c00
ENDCHAR
-STARTCHAR C177
+STARTCHAR phi
ENCODING 187
SWIDTH 600 0
DWIDTH 15 0
@@ -2559,7 +2873,7 @@
0c00
0c00
ENDCHAR
-STARTCHAR C177
+STARTCHAR chi
ENCODING 188
SWIDTH 600 0
DWIDTH 15 0
@@ -2578,7 +2892,7 @@
6600
c300
ENDCHAR
-STARTCHAR C167
+STARTCHAR psi
ENCODING 189
SWIDTH 600 0
DWIDTH 15 0
@@ -2598,7 +2912,7 @@
0600
0600
ENDCHAR
-STARTCHAR C167
+STARTCHAR omega
ENCODING 190
SWIDTH 600 0
DWIDTH 15 0
@@ -2612,7 +2926,7 @@
6660
1f80
ENDCHAR
-STARTCHAR C160
+STARTCHAR not
ENCODING 191
SWIDTH 666 0
DWIDTH 15 0
@@ -2625,7 +2939,7 @@
03
03
ENDCHAR
-STARTCHAR C161
+STARTCHAR and
ENCODING 192
SWIDTH 600 0
DWIDTH 15 0
@@ -2641,7 +2955,7 @@
c0c0
c0c0
ENDCHAR
-STARTCHAR C161
+STARTCHAR or
ENCODING 193
SWIDTH 600 0
DWIDTH 15 0
@@ -2657,7 +2971,7 @@
1e00
0c00
ENDCHAR
-STARTCHAR C166
+STARTCHAR forall
ENCODING 194
SWIDTH 600 0
DWIDTH 15 0
@@ -2678,7 +2992,7 @@
0c00
0c00
ENDCHAR
-STARTCHAR C167
+STARTCHAR exists
ENCODING 195
SWIDTH 600 0
DWIDTH 15 0
@@ -2699,7 +3013,7 @@
ff80
ff80
ENDCHAR
-STARTCHAR C166
+STARTCHAR And
ENCODING 196
SWIDTH 600 0
DWIDTH 15 0
@@ -2721,7 +3035,7 @@
4020
c030
ENDCHAR
-STARTCHAR C197
+STARTCHAR lceil
ENCODING 197
SWIDTH 600 0
DWIDTH 15 0
@@ -2743,7 +3057,7 @@
c0
c0
ENDCHAR
-STARTCHAR C197
+STARTCHAR rceil
ENCODING 198
SWIDTH 600 0
DWIDTH 15 0
@@ -2765,7 +3079,7 @@
03
03
ENDCHAR
-STARTCHAR C197
+STARTCHAR lfloor
ENCODING 199
SWIDTH 600 0
DWIDTH 15 0
@@ -2787,7 +3101,7 @@
ff
ff
ENDCHAR
-STARTCHAR C197
+STARTCHAR rfloor
ENCODING 200
SWIDTH 600 0
DWIDTH 15 0
@@ -2851,7 +3165,7 @@
c000
c000
ENDCHAR
-STARTCHAR C203
+STARTCHAR lbrakk
ENCODING 203
SWIDTH 600 0
DWIDTH 15 0
@@ -2872,7 +3186,7 @@
ff
ff
ENDCHAR
-STARTCHAR C204
+STARTCHAR rbrakk
ENCODING 204
SWIDTH 600 0
DWIDTH 15 0
@@ -2903,7 +3217,7 @@
e0
e0
ENDCHAR
-STARTCHAR C177
+STARTCHAR in
ENCODING 206
SWIDTH 600 0
DWIDTH 15 0
@@ -2922,7 +3236,7 @@
3f80
1f80
ENDCHAR
-STARTCHAR C161
+STARTCHAR subseteq
ENCODING 207
SWIDTH 600 0
DWIDTH 15 0
@@ -2940,11 +3254,11 @@
7fe0
7fe0
ENDCHAR
-STARTCHAR C161
+STARTCHAR inter
ENCODING 208
SWIDTH 600 0
DWIDTH 15 0
-BBX 10 12 1 0
+BBX 10 11 1 1
BITMAP
1e00
7f80
@@ -2957,13 +3271,12 @@
c0c0
c0c0
c0c0
-c0c0
ENDCHAR
-STARTCHAR C161
+STARTCHAR union
ENCODING 209
SWIDTH 600 0
DWIDTH 15 0
-BBX 10 12 1 0
+BBX 10 11 1 0
BITMAP
c0c0
c0c0
@@ -2973,12 +3286,11 @@
c0c0
c0c0
c0c0
-c0c0
e1c0
7f80
1e00
ENDCHAR
-STARTCHAR C197
+STARTCHAR Inter
ENCODING 210
SWIDTH 600 0
DWIDTH 15 0
@@ -3000,7 +3312,7 @@
c0c0
c0c0
ENDCHAR
-STARTCHAR C197
+STARTCHAR Union
ENCODING 211
SWIDTH 600 0
DWIDTH 15 0
@@ -3022,11 +3334,11 @@
7f80
1e00
ENDCHAR
-STARTCHAR C161
+STARTCHAR sqinter
ENCODING 212
SWIDTH 600 0
DWIDTH 15 0
-BBX 10 12 1 0
+BBX 10 11 1 1
BITMAP
ffc0
ffc0
@@ -3039,13 +3351,12 @@
c0c0
c0c0
c0c0
-c0c0
ENDCHAR
-STARTCHAR C161
+STARTCHAR squnion
ENCODING 213
SWIDTH 600 0
DWIDTH 15 0
-BBX 10 12 1 0
+BBX 10 11 1 0
BITMAP
c0c0
c0c0
@@ -3056,11 +3367,10 @@
c0c0
c0c0
c0c0
-c0c0
ffc0
ffc0
ENDCHAR
-STARTCHAR C197
+STARTCHAR Sqinter
ENCODING 214
SWIDTH 600 0
DWIDTH 15 0
@@ -3082,7 +3392,7 @@
c0c0
c0c0
ENDCHAR
-STARTCHAR C197
+STARTCHAR Squnion
ENCODING 215
SWIDTH 600 0
DWIDTH 15 0
@@ -3104,11 +3414,11 @@
ffc0
ffc0
ENDCHAR
-STARTCHAR C161
+STARTCHAR bottom
ENCODING 216
SWIDTH 600 0
DWIDTH 15 0
-BBX 12 12 1 0
+BBX 12 10 1 0
BITMAP
0600
0600
@@ -3118,12 +3428,10 @@
0600
0600
0600
-0600
-0600
fff0
fff0
ENDCHAR
-STARTCHAR C161
+STARTCHAR doteq
ENCODING 217
SWIDTH 600 0
DWIDTH 15 0
@@ -3139,7 +3447,7 @@
fff0
fff0
ENDCHAR
-STARTCHAR C177
+STARTCHAR equiv
ENCODING 218
SWIDTH 600 0
DWIDTH 15 0
@@ -3154,7 +3462,7 @@
ff80
ff80
ENDCHAR
-STARTCHAR C161
+STARTCHAR noteq
ENCODING 219
SWIDTH 600 0
DWIDTH 15 0
@@ -3173,7 +3481,7 @@
1800
1800
ENDCHAR
-STARTCHAR C161
+STARTCHAR sqsubset
ENCODING 220
SWIDTH 600 0
DWIDTH 15 0
@@ -3188,7 +3496,7 @@
ffe0
ffe0
ENDCHAR
-STARTCHAR C161
+STARTCHAR sqsubseteq
ENCODING 221
SWIDTH 600 0
DWIDTH 15 0
@@ -3206,7 +3514,7 @@
ffe0
ffe0
ENDCHAR
-STARTCHAR C177
+STARTCHAR prec
ENCODING 222
SWIDTH 600 0
DWIDTH 15 0
@@ -3225,7 +3533,7 @@
00c0
0040
ENDCHAR
-STARTCHAR C177
+STARTCHAR preceq
ENCODING 223
SWIDTH 600 0
DWIDTH 15 0
@@ -3246,7 +3554,7 @@
ffc0
ffc0
ENDCHAR
-STARTCHAR C177
+STARTCHAR succ
ENCODING 224
SWIDTH 600 0
DWIDTH 15 0
@@ -3265,7 +3573,7 @@
c000
8000
ENDCHAR
-STARTCHAR C161
+STARTCHAR approx
ENCODING 225
SWIDTH 600 0
DWIDTH 15 0
@@ -3280,7 +3588,7 @@
c7f0
01c0
ENDCHAR
-STARTCHAR C161
+STARTCHAR sim
ENCODING 226
SWIDTH 600 0
DWIDTH 15 0
@@ -3291,7 +3599,7 @@
c7f0
01c0
ENDCHAR
-STARTCHAR C161
+STARTCHAR simeq
ENCODING 227
SWIDTH 600 0
DWIDTH 15 0
@@ -3305,7 +3613,7 @@
fff0
fff0
ENDCHAR
-STARTCHAR C177
+STARTCHAR le
ENCODING 228
SWIDTH 600 0
DWIDTH 15 0
@@ -3324,7 +3632,7 @@
ff80
ff80
ENDCHAR
-STARTCHAR C177
+STARTCHAR ccolon
ENCODING 229
SWIDTH 600 0
DWIDTH 15 0
@@ -3358,7 +3666,7 @@
1c00
0c00
ENDCHAR
-STARTCHAR hline
+STARTCHAR midarrow
ENCODING 231
SWIDTH 600 0
DWIDTH 15 0
@@ -3405,7 +3713,7 @@
0700
0300
ENDCHAR
-STARTCHAR doublehline
+STARTCHAR Midarrow
ENCODING 234
SWIDTH 600 0
DWIDTH 15 0
@@ -3439,7 +3747,7 @@
0700
0600
ENDCHAR
-STARTCHAR C161
+STARTCHAR bow
ENCODING 236
SWIDTH 600 0
DWIDTH 15 0
@@ -3450,7 +3758,7 @@
e0e0
c060
ENDCHAR
-STARTCHAR C161
+STARTCHAR mapsto
ENCODING 237
SWIDTH 600 0
DWIDTH 15 0
@@ -3467,7 +3775,7 @@
c1c0
0180
ENDCHAR
-STARTCHAR C161
+STARTCHAR leadsto
ENCODING 238
SWIDTH 600 0
DWIDTH 15 0
@@ -3484,7 +3792,7 @@
00e0
00c0
ENDCHAR
-STARTCHAR C167
+STARTCHAR up
ENCODING 239
SWIDTH 600 0
DWIDTH 15 0
@@ -3504,7 +3812,7 @@
0c00
0c00
ENDCHAR
-STARTCHAR C167
+STARTCHAR down
ENCODING 240
SWIDTH 600 0
DWIDTH 15 0
@@ -3524,7 +3832,7 @@
1e00
0c00
ENDCHAR
-STARTCHAR C161
+STARTCHAR notin
ENCODING 241
SWIDTH 600 0
DWIDTH 15 0
@@ -3545,7 +3853,7 @@
7f80
6000
ENDCHAR
-STARTCHAR C175
+STARTCHAR times
ENCODING 242
SWIDTH 600 0
DWIDTH 15 0
@@ -3563,7 +3871,7 @@
6060
c030
ENDCHAR
-STARTCHAR plus
+STARTCHAR oplus
ENCODING 243
SWIDTH 600 0
DWIDTH 15 0
@@ -3584,7 +3892,7 @@
1fe0
0780
ENDCHAR
-STARTCHAR plus
+STARTCHAR ominus
ENCODING 244
SWIDTH 600 0
DWIDTH 15 0
@@ -3605,7 +3913,7 @@
1fe0
0780
ENDCHAR
-STARTCHAR plus
+STARTCHAR otimes
ENCODING 245
SWIDTH 600 0
DWIDTH 15 0
@@ -3626,7 +3934,7 @@
1fe0
0780
ENDCHAR
-STARTCHAR plus
+STARTCHAR oslash
ENCODING 246
SWIDTH 600 0
DWIDTH 15 0
@@ -3647,7 +3955,7 @@
1fe0
0780
ENDCHAR
-STARTCHAR C161
+STARTCHAR subset
ENCODING 247
SWIDTH 600 0
DWIDTH 15 0
@@ -3662,7 +3970,7 @@
7fe0
1fe0
ENDCHAR
-STARTCHAR C161
+STARTCHAR infinity
ENCODING 248
SWIDTH 600 0
DWIDTH 15 0
@@ -3677,7 +3985,7 @@
7cf8
3870
ENDCHAR
-STARTCHAR C161
+STARTCHAR box
ENCODING 249
SWIDTH 600 0
DWIDTH 15 0
@@ -3696,7 +4004,7 @@
fff0
fff0
ENDCHAR
-STARTCHAR C161
+STARTCHAR diamond
ENCODING 250
SWIDTH 600 0
DWIDTH 15 0
@@ -3716,7 +4024,7 @@
0700
0200
ENDCHAR
-STARTCHAR C161
+STARTCHAR circ
ENCODING 251
SWIDTH 600 0
DWIDTH 15 0
@@ -3731,7 +4039,7 @@
7e
3c
ENDCHAR
-STARTCHAR C161
+STARTCHAR bullet
ENCODING 252
SWIDTH 600 0
DWIDTH 15 0
@@ -3746,7 +4054,7 @@
7e
3c
ENDCHAR
-STARTCHAR C253
+STARTCHAR parallel
ENCODING 253
SWIDTH 600 0
DWIDTH 15 0
@@ -3768,7 +4076,7 @@
cc
cc
ENDCHAR
-STARTCHAR C254
+STARTCHAR surd
ENCODING 254
SWIDTH 600 0
DWIDTH 15 0
@@ -3786,7 +4094,7 @@
1e00
0c00
ENDCHAR
-STARTCHAR plus
+STARTCHAR copyright
ENCODING 255
SWIDTH 600 0
DWIDTH 15 0