On 19/03/10 08:36, [email protected] wrote:
> And I tried the way to remove the overloaded constant count and the one
> left in the library list is exact what I expected. Unfortunately, I have
> to solve some problems that appear because some theorems in
> extra_pred_setTheory could not be recognized by HOL any more. I'm trying
> to find a way to solve this problem...
I think you have two options:
1. Upgrade to the repository version of HOL. See
http://hol.sourceforge.net/anonymous-svn.html
for instructions on how to do this.
2. Update your version of examples/miller/formalize/extra_pred_setScript.sml:
a. Delete the definition of count on line 99
b. Delete the theorem IN_COUNT on lines 951-954
c. Rebuild the prob theories by
cd examples/miller/miller
../../../bin/Holmake
Michael
------------------------------------------------------------------------------
Download Intel® Parallel Studio Eval
Try the new software tools for yourself. Speed compiling, find bugs
proactively, and fine-tune applications for parallel performance.
See why Intel Parallel Studio got high marks during beta.
http://p.sf.net/sfu/intel-sw-dev
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
