1 # Title: Distribution/lib/scripts/symbolinput.pl |
1 # Title: lib/scripts/symbolinput.pl |
2 # ID: $Id$ |
2 # ID: $Id$ |
3 # Author: Markus Wenzel, David von Oheimb |
3 # Author: Markus Wenzel and David von Oheimb, TU Muenchen |
4 # Copyright 1996 Technische Universitaet Muenchen |
|
5 # |
4 # |
6 # translate symbols into \<...> sequences. |
5 # Translate symbols into \<...> sequences. Please keep consistent |
7 # table must be consistent with Pure/Syntax/symbol_font.ML |
6 # with Pure/Syntax/symbol_font.ML! |
8 |
7 |
9 %tab = ( |
8 %tab = ( |
10 "\xa1", "\\\\<Gamma>", |
9 "\xa1", "\\\\<Gamma>", |
11 "\xa2", "\\\\<Delta>", |
10 "\xa2", "\\\\<Delta>", |
12 "\xa3", "\\\\<Theta>", |
11 "\xa3", "\\\\<Theta>", |
91 "\xf2", "\\\\<times>", |
90 "\xf2", "\\\\<times>", |
92 "\xf3", "\\\\<oplus>", |
91 "\xf3", "\\\\<oplus>", |
93 "\xf4", "\\\\<ominus>", |
92 "\xf4", "\\\\<ominus>", |
94 "\xf5", "\\\\<otimes>", |
93 "\xf5", "\\\\<otimes>", |
95 "\xf6", "\\\\<oslash>", |
94 "\xf6", "\\\\<oslash>", |
96 "\xf7", "\\\\<natural>", |
95 "\xf7", "\\\\<subset>", |
97 "\xf8", "\\\\<infinity>", |
96 "\xf8", "\\\\<infinity>", |
98 "\xf9", "\\\\<box>", |
97 "\xf9", "\\\\<box>", |
99 "\xfa", "\\\\<diamond>", |
98 "\xfa", "\\\\<diamond>", |
100 "\xfb", "\\\\<circ>", |
99 "\xfb", "\\\\<circ>", |
101 "\xfc", "\\\\<bullet>", |
100 "\xfc", "\\\\<bullet>", |