Hi,guys
I had resolved this question. I substituted src file in
https://github.com/HOL-Theorem-Prover/HOL for src in HOL4 directory, and start
HOL4 by pointing hol\bin\hol.bat. Then, it worked.
Message: 2
Date: Wed, 2 Mar 2016 10:18:04 +0800
From: " ?? " <956066...@qq.com>
Subject: Re: [Hol-info] How to transform list format from "(cx l q p)"
to "l"
To: " hol-info " <hol-info@lists.sourceforge.net>
Message-ID: <tencent_2155785e19a3c2d91ec40...@qq.com>
Content-Type: text/plain; charset="gb18030"
Thank you for your reply!
My version of HOL4 is HOL-4 [Kananaskis 10 (stdknl, built Mon Nov 10 14:27:30
2014)], where Moscow ML version 2.01 (January 2004). Then from
https://hol-theorem-prover.org/#get, I installed PolyML5.6-32bit, and pointed
""bin/build". Then I got HOL-4 [Kananaskis 10 (stdknl, built Mon Feb 29
21:47:05 2016)],where Moscow ML version 2.01 (January 2004).
I Opened HOL4, print"open listTheory;", I still can't use LENGTH_TAKE_EQ, it
responed "Unbound value component: listTheory.LENGTH_TAKE_EQ". I had downloaded
the files in https://github.com/HOL-Theorem-Prover/HOL. How to add it to HOL4's
directory? After that ,I could print "open listTheory;" in HOL4, and use
LENGTH_TAKE_EQ.
Thanks.
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
