# HG changeset patch # User oheimb # Date 918826856 -3600 # Node ID 25d41c1183041550446e352279423b8a58021081 # Parent 218733fb6987c30bb7381d94ac3529399845eadf renamed space2 to spacespace diff -r 218733fb6987 -r 25d41c118304 lib/encodings/isabelle-0 --- a/lib/encodings/isabelle-0 Fri Feb 12 13:56:21 1999 +0100 +++ b/lib/encodings/isabelle-0 Fri Feb 12 14:40:56 1999 +0100 @@ -24,7 +24,7 @@ 160: -space2 +spacespace Gamma Delta Theta diff -r 218733fb6987 -r 25d41c118304 lib/fonts/isabelle14.bdf --- a/lib/fonts/isabelle14.bdf Fri Feb 12 13:56:21 1999 +0100 +++ b/lib/fonts/isabelle14.bdf Fri Feb 12 14:40:56 1999 +0100 @@ -1741,7 +1741,7 @@ ff80 ff80 ENDCHAR -STARTCHAR space2 +STARTCHAR spacespace ENCODING 160 SWIDTH 264 0 DWIDTH 9 0 diff -r 218733fb6987 -r 25d41c118304 lib/fonts/isabelle24.bdf --- a/lib/fonts/isabelle24.bdf Fri Feb 12 13:56:21 1999 +0100 +++ b/lib/fonts/isabelle24.bdf Fri Feb 12 14:40:56 1999 +0100 @@ -2333,7 +2333,7 @@ fff0 fff0 ENDCHAR -STARTCHAR space2 +STARTCHAR spacespace ENCODING 160 SWIDTH 600 0 DWIDTH 15 0 diff -r 218733fb6987 -r 25d41c118304 lib/scripts/feeder.pl --- a/lib/scripts/feeder.pl Fri Feb 12 13:56:21 1999 +0100 +++ b/lib/scripts/feeder.pl Fri Feb 12 14:40:56 1999 +0100 @@ -13,7 +13,7 @@ %tab = ( #GENERATED TEXT FOLLOWS - Do not edit! - "\xa0", "\\", + "\xa0", "\\", "\xa1", "\\", "\xa2", "\\", "\xa3", "\\", diff -r 218733fb6987 -r 25d41c118304 lib/scripts/symbolinput.pl --- a/lib/scripts/symbolinput.pl Fri Feb 12 13:56:21 1999 +0100 +++ b/lib/scripts/symbolinput.pl Fri Feb 12 14:40:56 1999 +0100 @@ -6,7 +6,7 @@ %tab = ( #GENERATED TEXT FOLLOWS - Do not edit! - "\xa0", "\\", + "\xa0", "\\", "\xa1", "\\", "\xa2", "\\", "\xa3", "\\",