[ProofPower] PPRefinement Example in 2.9.1w2

[Rob Arthan]

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 usual place:

http://www.lemma-one.com/ProofPower/examples/PPRefinement.tgz

If you need the earlier version, you can find it here:

http://www.lemma-one.com/ProofPower/examples/versions

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.

Regards,

Rob.