On 10-12-27 09:48 AM, Grace wrote: > 1. When I install the HOL4 Kananaskis 6 in WINDOWS XP system, it can > operational but garbled as follows: > > val REAL_ARCH_LEAST = > > |- 鈭€y. 0 < y 鈬?鈭€x. 0 鈮?x 鈬?鈭僴. &n * y 鈮?x 鈭?x < &SUC n * y > > : thm > > val REAL_LT_IMP_LE = |- 鈭€x y. x < y 鈬?x 鈮?y : thm
Windows console can do UTF-8 but does not default to it. Do this before starting hol: chcp 65001 Beware that even then, the console font lacks some pretty common symbols. ------------------------------------------------------------------------------ Learn how Oracle Real Application Clusters (RAC) One Node allows customers to consolidate database storage, standardize their database environment, and, should the need arise, upgrade to a full multi-node Oracle RAC database without downtime or disruption http://p.sf.net/sfu/oracle-sfdevnl _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
