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

Reply via email to