theory Export imports Frontend begin definition ascii :: "integer \ char" where "ascii = char_of" definition ordinal :: "char \ integer" where "ordinal = of_char" export_code process binary artifact disassemble ascii ordinal in SML module_name Span file_prefix span end