Re: a problem, could you please help me!

[Sam Owre <owre@csl.sri.com>]

Dear Jihan,

This is a bug, though I have been unable to reproduce it in PVS 3.0.
When this error happens again, could you try the following:

 - If the minibuffer contains the line
   SPC-scroll, I-ignore, K-keep, A-abort sends and keep or B-break:
   type a "b".
 - go to the end of the *pvs* buffer
 - type ":bt" at the pvs prompt, and send me the results

I think the cause of this is that one of your "IMPLIES" is spelled
incorrectly, but it should just give a parse error, which is what I get
when I try this.

Thanks,
Sam