Mercurial Mercurial > repos > isabelle / diff
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.
lib/fonts/isabelle24.bdf
changeset 3064 f04f93e5c0a9
parent 2791 b65da0c53d94
child 3082 9b68848654bf 
--- 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
isabelle