For some reason in my hol session system libraries are no longer visible. If I directly type into the hol console:
> pred_setTheory; poly: : error: Value or constructor (pred_setTheory) has not been declared Found near pred_setTheory Static Errors But when I evaluates through emacs 'M-h' 'M-r' everything still works. The only difference I can tell is that in the emacs case hol is reading and evaluating a temporarily created script sml file. I definitely remember I could do the above in the hol console as well and I had not played with any settings/env variables intentionally. It is possible that sometimes by hitting the wrong key sequence in emacs I had sent very erroneous strings to be evaluated. Where should I look to resolve this? Thanks, Haitao
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
