It is my plan to make some experimental releases of OpenProofPower leading towards the next stable version over the next few months. I have just uploaded an experimental release to:
http://www.lemma-one.com/ProofPower/getting/experimental/OpenProofPower-2.9.1w2.rda.110226.tgz The idea is that an experimental release is a step toward the next stable version (2.9.2 in this case). There may be additional working versions 2.9.1wN to fix problems, but the interfaces in the working versions will be stable within one release. The experimental release directory will also contain changed versions of other items, e.g., the mathematical case studies, if those need to be updated for the experimental release. See the CHANGES file for more details, but some noteworthy changes relative to 2.9.1w2 are: a) Alongside the functions set_pc, set_merge_pcs, PC_T, MERGE_PCS_T, etc. there are now functions set_extend_pc, set_extend_pcs, EXTEND_PC_T, EXTEND_PCS_T etc., that extend the current proof context rather than overwrite it. This facilitates proof contexts that just change the behaviour of particular proof procedures like forward chaining. b) A variable capture problem in %implies%_match_mp_rule1 that made forward chaining fail has been addressed in a new rule %implies%_match_mp_rule2. The new behaviour has been adopted as the default, but this can make some existing proofs break. Component proof contexts "'mmp1" and "'mmp2" are provided that let you switch between the new and old behaviour. Using, set_extend_pc"'mmp1" or EXTEND_PC_T "'mmp1" will revert to the old behaviour and gives a quick way of fixing any broken proof scripts. c) A new feature in xpp: the Window menu now has Show/Hide Journal as well as Show/Hide Script. Show/Hide Script and Command/Execute line were originally intended for doing demonstrations, typically on an overhead projector, but I have found them both very useful in doing proofs and development generally. When you are developing stuff, Show/Hide Journal lets you see more of what you are working on when you are not interested in the output from ProofPower (or HOL Light or whatever). If you update your app-defaults/XppKeyboard file you can switch between the three different views at lightning speed with Ctrl+H and Ctrl+J. d) The higher-order matching interfaces for HOL that were provided are in what should be their final form. ho_match is now called simple_ho_match and implements a better-defined specification (it expects pattern and target to be beta-reduced, but carries out eta-conversion as necessary to make the match work). simple_ho_eq_match_conv now works. Thanks to Mark Adams for pointing out that the new behaviour of undo in xpp was a little counter-intuitive as a result of a lsat-minute change that went missing and to Roger Jones for input on the work on forward chaining. Feedback on any of this is welcome. Regards, Rob
_______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
