equal
deleted
inserted
replaced
2 # ID: $Id$ |
2 # ID: $Id$ |
3 # Author: Markus Wenzel, David von Oheimb |
3 # Author: Markus Wenzel, David von Oheimb |
4 # Copyright 1996 Technische Universitaet Muenchen |
4 # Copyright 1996 Technische Universitaet Muenchen |
5 # |
5 # |
6 # translate symbols into \<...> sequences. |
6 # translate symbols into \<...> sequences. |
|
7 # table must be consistent with Pure/Syntax/symbol_font.ML |
7 |
8 |
8 %tab = ( |
9 %tab = ( |
9 "\xa1", "\\\\<Gamma>", |
10 "\xa1", "\\\\<Gamma>", |
10 "\xa2", "\\\\<Delta>", |
11 "\xa2", "\\\\<Delta>", |
11 "\xa3", "\\\\<Theta>", |
12 "\xa3", "\\\\<Theta>", |