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:
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
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
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.
Proofpower mailing list