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

Reply via email to