I have hacked the HOL-Light files parser.ml and printer.ml to provide some
experimental support for non-ascii ("eight-bit") chars in terms, see
http://csee.essex.ac.uk/staff/norbert/hol_light_non_ascii/
It is not a proper Unicode mode or anything like that, and in particular you
cannot mix ascii and non-ascii characters in one identifier unless you use an
underscore character to join them. But it should support some typical
use-cases such as identifiers made from Greek letters or mathematical symbols.
Please email me directly if you have comments/ find bugs - I am not a regular
reader of this mailing list.
Norbert.
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
