# HG changeset patch
# User wenzelm
# Date 856539349 -3600
# Node ID 585cd2311a98578c76f2dc5c695fbccbf01a06b3
# Parent  e2908f8edc8ddb1a8a9fe85ffc959da4f9e84303
replaced natural by subset;

diff -r e2908f8edc8d -r 585cd2311a98 lib/fonts/isacb24.bdf
--- 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
diff -r e2908f8edc8d -r 585cd2311a98 lib/fonts/isacr14.bdf
--- 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
diff -r e2908f8edc8d -r 585cd2311a98 lib/scripts/symbolinput.pl
--- 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>",
diff -r e2908f8edc8d -r 585cd2311a98 src/Pure/Syntax/symbol_font.ML
--- 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"
 ];