[ProofPower] ml library functions from pp command line

["Mark"]

That's because ProofPower overwrites PolyML's ML structure List with its
own, for holding theory about HOL lists.  I'm not sure if anything can be
done about this without alterning the ProofPower build process (and, say,
creating a copy of PolyML's List with a name not used by ProofPower).

Mark.

on 22/2/13 12:33 PM, Yuhui Lin <Y.H.Lin-2 at sms.ed.ac.uk> wrote:

> Hi,
>
> I'm trying to build a programme on the top of proof power with the pp
> interface. I need a full polyML library from the pp interface, but I can't
> use some functions which are defined in polyML, e.g List.exists. Any
> suggestion ?
>
> Thanks in advance.
>
> best,
> Yuhui
> --
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
> _______________________________________________
> Proofpower mailing list
> Proofpower at lemma-one.com
> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
>
>
>