[MetaPRL Users] Term extraction problem

[Aleksey Nogin]

On 07.09.2006 10:50, Wojtek Moczydlowski wrote:

> Well, I don't have any proofs yet to save. But, unfortunately, even after
> this I still get the same message.

Hm, this all is really strange. Can you may be email me the transcript 
of the whole MetaPRL session where this happens, so that I can see if 
there is something unusual on the way?

> Maybe the information that even when 
> I complete the proof
> and * appears everywhere, after I quit and come back to the editor, the *
> disappears and only ? remaing is useful?

No, this is always the case - MetaPRL only saves the proof outline (not 
the expansion into primitive proof steps), and when you restart, MetaPRL 
does not know the status of the proof until you re-run it.

BTW, to re-run a proof, cd into it and run "expand()", or cd into a 
theory and use "expand_all()" to re-run all the proofs in that theory.

Aleksey