Pure/General/symbol.ML;
authorwenzelm
Thu Jan 14 12:32:00 1999 +0100 (1999-01-14)
changeset 6126826576f7e137
parent 6125 59507030d953
child 6127 ece970eb5850
Pure/General/symbol.ML;
Admin/fixencoding
     1.1 --- a/Admin/fixencoding	Thu Jan 14 12:23:00 1999 +0100
     1.2 +++ b/Admin/fixencoding	Thu Jan 14 12:32:00 1999 +0100
     1.3 @@ -135,7 +135,7 @@
     1.4  
     1.5  # patch files
     1.6  
     1.7 -&patch_file("Pure/Syntax/symbol.ML", $ml_tab);
     1.8 +&patch_file("Pure/General/symbol.ML", $ml_tab);
     1.9  &patch_file("Distribution/lib/scripts/symbolinput.pl", $perl_tab);
    1.10  &patch_file("Distribution/lib/scripts/feeder.pl", $perl_tab);
    1.11  #&patch_file("Distribution/lib/scripts/symboloutput.pl", $perl_revtab);