Re: [ProofPower] use library function with special symbol
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
[ProofPower] use library function with special symbol
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. best, Yuhui -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
