[ProofPower] ProofPower Update
Dear All, I plan to make a new ProofPower release shortly. In the meantime, if you want the state of the art, I uploaded an experimental version built from the latest source. You can find this here: http://www.lemma-one.com/ProofPower/getting/experimental/ The main reason for the experimental release was because I hadn't updated the Mathematical Case Studies listed on the examples page (http://www.lemma-one.com/ProofPower/examples/examples.html) and I wanted to upload the latest versions of those for various people to read. So the main changes in ProofPower are in ProofPower-HOL. Specifically, I think higher-order matching is well-tested and stable now. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] ProofPower Update
Rob, On Thursday 09 Aug 2012 10:26, Rob Arthan wrote: I plan to make a new ProofPower release shortly. In the meantime, if you want the state of the art, I uploaded an experimental version built from the latest source. You can find this here: http://www.lemma-one.com/ProofPower/getting/experimental/ It that any different from what you get building from the RCS archive in your dropbox? Can I build MathsEgs from that RCS? [actually, I just tried but I see that the makefile for maths_egs isn't compliant with the pattern used in that system (no inst target, and the bld target fails). VERY MINOR COMMENT Seems odd that the directory in which one builds is called pp and the one in which one installs is ppdev. Shouldn't it be the other way round? Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] ProofPower Update
Rob, My theories fail to build on the latest version of maths_egs because I have been using R_plus_ops_thm and R_plus_group_thm which were in wrk068 but are no longer. Looks like you have just changed some names, is that right? Roger Jones ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
