Hi everyone,
I have 2 questions:
1. When I install the HOL4Kananaskis6 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
before installing the HOL4 Kananaskis 6, I installed mosml-2.01-1.exe
successfully.
What’s the problem?
2. What does “val seq_list l = Define`seq_list l = {(I,j) | (i < j) /\ (EL i l
> EL j l)}`;” mean?
Thanks,
--Grace------------------------------------------------------------------------------
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
