Added support for UTF-8

[imbrem]

Some design decisions:

• Nonterminals can now be any UTF-8 strings which do not contain any ASCII special characters, which are defined to be all ASCII characters (i.e. with codepoint ≤ 127) other than ['0'-'9']|['a'-'z']|['A'-'Z']
• Nonterminals with Unicode names are escaped into TeX by mapping codepoints to base-16 shifted up by 16, i.e. with digits ghijklmnopqrstuv. So λ2, which is at codepoint 03bb, becomes \ottjrrTwo (with the default prefix \ott).
• Invalid UTF-8 leads to an exception being thrown

[dc-mak]

Peter says

• Please run regressions
• State what the output is for theorem prover backends
• Please state what happens with index variables Γ1 .. Γn and other things.