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.

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Proofpower mailing list

Reply via email to