OpenProofPower version 2.9.1w2 incorporated a fix to a bug that made several of
the Z proof contexts fail to simplify certain expressions involving Z set
comprehensions. The PPRefinement example was sensitive to this fix. I have just
posted a replacement for PPRefinement.tgz that works with 2.9.1w2. It is in the
If you need the earlier version, you can find it here:
Thanks to Phil who found and fixed the bug and apologies from me for forgetting
to update PPRefinement.tgz when I released 2.9.1w2.
Proofpower mailing list