On 19/09/13 16:25, YuHui Lin wrote: > Hi, > > I notice that some function names need to be changed when using the key word > 'use_file' to include ML files, e.g. EQUAL becomes E%Q%UAL. I wonder why ? > Is there anything else I need to keep in mind when using use_fie ? Many > thanks. > use_file is for processing files in the ProofPower extended ML, which supports an extended character set. The usual way of preparing such files is to use the editor Xpp which understands the extended character set and then run the file through docsml before loading it with use_file.
Xpp supports interactive development of a document while running ProofPower, see: ProofPower Document Preparation, usr001.pdf The Xpp User Guide, usr031.pdf Roger Jones _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com