Yuhui,

On 12 Aug 2013, at 17:16, YuHui Lin wrote:

> Hi,
> 
> I'm currently developing a system on the top of proof power.  I get an error 
> when reading a ml file with the keyword "use" in xpp. The error is caused by 
> the use of a library function containing a special symbol, i.e. 
> dest_simple_%lambda%. I am sure all the codes in the ML file is OK, as there 
> is no problem if I load the ml directly from xpp.  How I can resolve this ? 
> Thanks in advance.
> 

Use "use_file" rather than "use".

Regards,

Rob.

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to