--- a/lib/fonts/isacb24.bdf Fri Feb 21 16:35:30 1997 +0100
+++ b/lib/fonts/isacb24.bdf Fri Feb 21 16:35:49 1997 +0100
@@ -3768,26 +3768,20 @@
1fe0
0780
ENDCHAR
-STARTCHAR C247
+STARTCHAR C161
ENCODING 247
SWIDTH 600 0
DWIDTH 15 0
-BBX 7 14 1 0
+BBX 11 8 1 3
BITMAP
-c0
-c0
-c6
-ce
-de
-f6
-e6
-ce
-de
-f6
-e6
-c6
-06
-06
+1fe0
+7fe0
+e000
+c000
+c000
+e000
+7fe0
+1fe0
ENDCHAR
STARTCHAR C161
ENCODING 248
--- a/lib/fonts/isacr14.bdf Fri Feb 21 16:35:30 1997 +0100
+++ b/lib/fonts/isacr14.bdf Fri Feb 21 16:35:49 1997 +0100
@@ -2466,11 +2466,12 @@
ENCODING 221
SWIDTH 666 0
DWIDTH 9 0
-BBX 6 6 1 1
+BBX 6 7 1 0
BITMAP
fc
80
80
+80
fc
00
fc
@@ -2818,21 +2819,22 @@
2200
1c00
ENDCHAR
-STARTCHAR natural
+STARTCHAR subset
ENCODING 247
-SWIDTH 600 0
+SWIDTH 666 0
DWIDTH 9 0
-BBX 4 9 2 0
+BBX 6 10 1 -2
BITMAP
+7c
80
-90
-b0
-d0
-90
-b0
-d0
-90
-10
+80
+80
+7c
+00
+00
+00
+00
+00
ENDCHAR
STARTCHAR infinity
ENCODING 248
--- a/lib/scripts/symbolinput.pl Fri Feb 21 16:35:30 1997 +0100
+++ b/lib/scripts/symbolinput.pl Fri Feb 21 16:35:49 1997 +0100
@@ -1,10 +1,9 @@
-# Title: Distribution/lib/scripts/symbolinput.pl
+# Title: lib/scripts/symbolinput.pl
# ID: $Id$
-# Author: Markus Wenzel, David von Oheimb
-# Copyright 1996 Technische Universitaet Muenchen
+# Author: Markus Wenzel and David von Oheimb, TU Muenchen
#
-# translate symbols into \<...> sequences.
-# table must be consistent with Pure/Syntax/symbol_font.ML
+# Translate symbols into \<...> sequences. Please keep consistent
+# with Pure/Syntax/symbol_font.ML!
%tab = (
"\xa1", "\\\\<Gamma>",
@@ -93,7 +92,7 @@
"\xf4", "\\\\<ominus>",
"\xf5", "\\\\<otimes>",
"\xf6", "\\\\<oslash>",
- "\xf7", "\\\\<natural>",
+ "\xf7", "\\\\<subset>",
"\xf8", "\\\\<infinity>",
"\xf9", "\\\\<box>",
"\xfa", "\\\\<diamond>",
--- a/src/Pure/Syntax/symbol_font.ML Fri Feb 21 16:35:30 1997 +0100
+++ b/src/Pure/Syntax/symbol_font.ML Fri Feb 21 16:35:49 1997 +0100
@@ -2,8 +2,8 @@
ID: $Id$
Author: Markus Wenzel, TU Muenchen
-The Isabelle symbol font.
-enc_vector must be consistent with Distribution/lib/scripts/symbolinput.pl
+The Isabelle symbol font. Please keep enc_vector consistent with
+lib/scripts/symbolinput.pl!
*)
signature SYMBOL_FONT =
@@ -39,7 +39,7 @@
"bottom", "doteq", "equiv", "noteq", "sqsubset", "sqsubseteq", "prec", "preceq",
"succ", "succeq", "sim", "simeq", "le", "ge", "leftarrow", "midarrow",
"rightarrow", "Leftarrow", "Midarrow", "Rightarrow", "rrightarrow", "mapsto", "leadsto", "up",
- "down", "notin", "times", "oplus", "ominus", "otimes", "oslash", "natural",
+ "down", "notin", "times", "oplus", "ominus", "otimes", "oslash", "subset",
"infinity", "box", "diamond", "circ", "bullet", "parallel", "tick", "copyright"
];