equal
deleted
inserted
replaced
4 # symbolinput.pl - expand isabelle-0 encoded chars to \<...> sequences. |
4 # symbolinput.pl - expand isabelle-0 encoded chars to \<...> sequences. |
5 # |
5 # |
6 |
6 |
7 %tab = ( |
7 %tab = ( |
8 #GENERATED TEXT FOLLOWS - Do not edit! |
8 #GENERATED TEXT FOLLOWS - Do not edit! |
9 "\xa0", "\\<space2>", |
9 "\xa0", "\\<spacespace>", |
10 "\xa1", "\\<Gamma>", |
10 "\xa1", "\\<Gamma>", |
11 "\xa2", "\\<Delta>", |
11 "\xa2", "\\<Delta>", |
12 "\xa3", "\\<Theta>", |
12 "\xa3", "\\<Theta>", |
13 "\xa4", "\\<Lambda>", |
13 "\xa4", "\\<Lambda>", |
14 "\xa5", "\\<Pi>", |
14 "\xa5", "\\<Pi>", |