2016-06-10 文字の扱い Isabelle ダメ出し writeln "\<alpha>" とかはアプリケーションレベルでのサポート。よって、#"a" はcharだが、#"\<alpha>" はcharにならない。Poly/MLのUnicodeサポート状況によるが、Unicode文字を文字および文字列に使えるはずだが、ASCII頭で凝り固まっている。