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_simp
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 th
