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. _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
