# HG changeset patch
# User wenzelm
# Date 862324753 -7200
# Node ID f04f93e5c0a9245d10664202f640cee9d710516c
# Parent  963e3bf01799567890e1680a66bfb4b16dcc9129
added new chars;

diff -r 963e3bf01799 -r f04f93e5c0a9 lib/encodings/isabelle-0
--- a/lib/encodings/isabelle-0	Tue Apr 29 16:38:16 1997 +0200
+++ b/lib/encodings/isabelle-0	Tue Apr 29 16:39:13 1997 +0200
@@ -4,7 +4,24 @@
 # The isabelle-0 encoding table.
 #
 
-161:
+145:
+
+lless
+unlhd
+lhd
+rhd
+tturnstile
+langle
+rangle
+choice
+top
+Or
+ocdot
+iota
+upsilon
+Upsilon
+Xi
+space2
 Gamma
 Delta
 Theta
@@ -41,13 +58,10 @@
 forall
 exists
 And
-
-#lceil
-#rceil
-#lfloor
-#rfloor
-
-201:
+lceil
+rceil
+lfloor
+rfloor
 turnstile
 Turnstile
 lbrakk
diff -r 963e3bf01799 -r f04f93e5c0a9 lib/fonts/isabelle14.bdf
--- a/lib/fonts/isabelle14.bdf	Tue Apr 29 16:38:16 1997 +0200
+++ b/lib/fonts/isabelle14.bdf	Tue Apr 29 16:39:13 1997 +0200
@@ -1,7 +1,7 @@
 STARTFONT 2.1
 FONT -isabelle-fixed-medium-r-normal--14-140-75-75-m-90-isabelle-0
 SIZE 14 75 75
-FONTBOUNDINGBOX 9 14 4 -3
+FONTBOUNDINGBOX 10 14 4 -3
 STARTPROPERTIES 22
 FONTNAME_REGISTRY ""
 FOUNDRY "Isabelle"
@@ -26,7 +26,7 @@
 CAP_HEIGHT 9
 X_HEIGHT 7
 ENDPROPERTIES
-CHARS 191
+CHARS 206
 STARTCHAR space
 ENCODING 32
 SWIDTH 600 0
@@ -837,7 +837,7 @@
 BBX 7 9 1 0
 BITMAP
 fe
-10
+92
 10
 10
 10
@@ -1497,13 +1497,258 @@
 64
 98
 ENDCHAR
-STARTCHAR space
-ENCODING 160
+STARTCHAR lless
+ENCODING 145
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 6 11 1 -1
+BITMAP
+04
+08
+10
+24
+48
+90
+48
+24
+10
+08
+04
+ENDCHAR
+STARTCHAR unlhd
+ENCODING 146
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 8 9 1 -1
+BITMAP
+03
+0d
+31
+c1
+31
+0d
+03
+00
+ff
+ENDCHAR
+STARTCHAR lhd
+ENCODING 147
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 8 7 1 1
+BITMAP
+03
+0d
+31
+c1
+31
+0d
+03
+ENDCHAR
+STARTCHAR rhd
+ENCODING 148
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 8 7 1 1
+BITMAP
+c0
+b0
+8c
+83
+8c
+b0
+c0
+ENDCHAR
+STARTCHAR tturnstile
+ENCODING 149
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 9 3 0
+BITMAP
+a0
+a0
+a0
+a0
+ff
+a0
+a0
+a0
+a0
+ENDCHAR
+STARTCHAR langle
+ENCODING 150
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 4 12 3 -2
+BITMAP
+10
+20
+20
+40
+40
+80
+80
+40
+40
+20
+20
+10
+ENDCHAR
+STARTCHAR rangle
+ENCODING 151
 SWIDTH 600 0
 DWIDTH 9 0
-BBX 1 1 0 0
+BBX 4 12 3 -2
+BITMAP
+80
+40
+40
+20
+20
+10
+10
+20
+20
+40
+40
+80
+ENDCHAR
+STARTCHAR choice
+ENCODING 152
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 6 12 1 -2
+BITMAP
+3c
+24
+24
+24
+24
+24
+24
+24
+24
+24
+24
+3c
+ENDCHAR
+STARTCHAR top
+ENCODING 153
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 7 6 1 2
+BITMAP
+fe
+10
+10
+10
+10
+10
+ENDCHAR
+STARTCHAR Or
+ENCODING 154
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 12 1 -2
+BITMAP
+82
+82
+82
+44
+44
+44
+28
+28
+28
+10
+10
+10
+ENDCHAR
+STARTCHAR ocdot
+ENCODING 155
+SWIDTH 240 0
+DWIDTH 9 0
+BBX 9 9 0 0
 BITMAP
-00
+1c00
+2200
+4100
+8080
+8880
+8080
+4100
+2200
+1c00
+ENDCHAR
+STARTCHAR iota
+ENCODING 156
+SWIDTH 168 0
+DWIDTH 9 0
+BBX 3 6 1 0
+BITMAP
+e0
+60
+60
+c0
+e0
+c0
+ENDCHAR
+STARTCHAR upsilon
+ENCODING 157
+SWIDTH 168 0
+DWIDTH 9 0
+BBX 7 7 1 0
+BITMAP
+c4
+62
+62
+62
+62
+64
+38
+ENDCHAR
+STARTCHAR Upsilon
+ENCODING 158
+SWIDTH 264 0
+DWIDTH 9 0
+BBX 8 10 0 -1
+BITMAP
+c3
+64
+38
+18
+18
+18
+18
+18
+18
+3c
+ENDCHAR
+STARTCHAR Xi
+ENCODING 159
+SWIDTH 264 0
+DWIDTH 9 0
+BBX 9 10 1 -1
+BITMAP
+ff80
+ff80
+8080
+0000
+1c00
+1c00
+0000
+8080
+ff80
+ff80
+ENDCHAR
+STARTCHAR space2
+ENCODING 160
+SWIDTH 264 0
+DWIDTH 9 0
+BBX 9 2 1 0
+BITMAP
+8880
+dd80
 ENDCHAR
 STARTCHAR Gamma
 ENCODING 161
@@ -1609,63 +1854,66 @@
 ENDCHAR
 STARTCHAR Phi
 ENCODING 167
-SWIDTH 240 0
+SWIDTH 264 0
 DWIDTH 9 0
-BBX 5 9 2 0
+BBX 10 10 1 -1
 BITMAP
-70
-20
-70
-a8
-a8
-a8
-70
-20
-70
+1e00
+0c00
+7f80
+ccc0
+ccc0
+ccc0
+ccc0
+7f80
+0c00
+1e00
 ENDCHAR
 STARTCHAR Psi
 ENCODING 168
 SWIDTH 264 0
 DWIDTH 9 0
-BBX 7 9 1 0
+BBX 10 10 1 -1
 BITMAP
-38
-10
-92
-54
-54
-54
-38
-10
-38
+1e00
+8c40
+ccc0
+ccc0
+ccc0
+ccc0
+7f80
+0c00
+0c00
+1e00
 ENDCHAR
 STARTCHAR Omega
 ENCODING 169
-SWIDTH 240 0
+SWIDTH 264 0
 DWIDTH 9 0
-BBX 7 9 1 0
+BBX 9 10 1 -1
 BITMAP
-38
-44
-82
-82
-82
-44
-28
-aa
-ee
+3e00
+6300
+c180
+c180
+c180
+c180
+6300
+3600
+9480
+f780
 ENDCHAR
 STARTCHAR alpha
 ENCODING 170
 SWIDTH 216 0
 DWIDTH 9 0
-BBX 8 6 0 0
+BBX 7 6 0 0
 BITMAP
-39
-49
-8e
+76
+9c
 8c
-8c
+88
+98
 76
 ENDCHAR
 STARTCHAR beta
@@ -2393,15 +2641,13 @@
 ENCODING 216
 SWIDTH 666 0
 DWIDTH 9 0
-BBX 7 8 1 0
+BBX 7 6 1 0
 BITMAP
 10
 10
 10
 10
 10
-10
-10
 fe
 ENDCHAR
 STARTCHAR doteq
diff -r 963e3bf01799 -r f04f93e5c0a9 lib/fonts/isabelle24.bdf
--- 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
diff -r 963e3bf01799 -r f04f93e5c0a9 lib/scripts/symbolinput.pl
--- a/lib/scripts/symbolinput.pl	Tue Apr 29 16:38:16 1997 +0200
+++ b/lib/scripts/symbolinput.pl	Tue Apr 29 16:39:13 1997 +0200
@@ -6,6 +6,22 @@
 
 %tab = (
 #GENERATED TEXT FOLLOWS - Do not edit!
+  "\x91", "\\<lless>",
+  "\x92", "\\<unlhd>",
+  "\x93", "\\<lhd>",
+  "\x94", "\\<rhd>",
+  "\x95", "\\<tturnstile>",
+  "\x96", "\\<langle>",
+  "\x97", "\\<rangle>",
+  "\x98", "\\<choice>",
+  "\x99", "\\<top>",
+  "\x9a", "\\<Or>",
+  "\x9b", "\\<ocdot>",
+  "\x9c", "\\<iota>",
+  "\x9d", "\\<upsilon>",
+  "\x9e", "\\<Upsilon>",
+  "\x9f", "\\<Xi>",
+  "\xa0", "\\<space2>",
   "\xa1", "\\<Gamma>",
   "\xa2", "\\<Delta>",
   "\xa3", "\\<Theta>",
@@ -42,10 +58,10 @@
   "\xc2", "\\<forall>",
   "\xc3", "\\<exists>",
   "\xc4", "\\<And>",
-  "\xc5", "\\<undef197>",
-  "\xc6", "\\<undef198>",
-  "\xc7", "\\<undef199>",
-  "\xc8", "\\<undef200>",
+  "\xc5", "\\<lceil>",
+  "\xc6", "\\<rceil>",
+  "\xc7", "\\<lfloor>",
+  "\xc8", "\\<rfloor>",
   "\xc9", "\\<turnstile>",
   "\xca", "\\<Turnstile>",
   "\xcb", "\\<lbrakk>",
diff -r 963e3bf01799 -r f04f93e5c0a9 src/Pure/Syntax/symbol_font.ML
--- a/src/Pure/Syntax/symbol_font.ML	Tue Apr 29 16:38:16 1997 +0200
+++ b/src/Pure/Syntax/symbol_font.ML	Tue Apr 29 16:39:13 1997 +0200
@@ -26,12 +26,28 @@
 
 (* tables *)
 
-val enc_start = 161;
+val enc_start = 145;
 val enc_end = 255;
 
 val enc_vector =
 [
 (* GENERATED TEXT FOLLOWS - Do not edit! *)
+  "lless",
+  "unlhd",
+  "lhd",
+  "rhd",
+  "tturnstile",
+  "langle",
+  "rangle",
+  "choice",
+  "top",
+  "Or",
+  "ocdot",
+  "iota",
+  "upsilon",
+  "Upsilon",
+  "Xi",
+  "space2",
   "Gamma",
   "Delta",
   "Theta",
@@ -68,10 +84,10 @@
   "forall",
   "exists",
   "And",
-  "undef197",
-  "undef198",
-  "undef199",
-  "undef200",
+  "lceil",
+  "rceil",
+  "lfloor",
+  "rfloor",
   "turnstile",
   "Turnstile",
   "lbrakk",