I have just completed a new experimental release of OpenProofPower. You can
find it here:
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 also contains 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 details of the changes relative to 2.9.1w2, but some
noteworthy changes relative to 2.9.1w2.rda.110727 are:
a) For visual compatibility with the ISO standard, a symbol for unary minus in
Z has been added to the font and defined as a synonym of the unary minus
written as a tilde in the theory z_numbers. The symbol displays and typesets as
short minus sign. %cat%/ (i.e., a frown followed by a backslash) is now defined
as an alias for distributed concatenation written %dcat% in the theory
b) In xpp, you can now switch dynamically between the horizontal and vertical
layout using a new item in the window geometry. N.b., this is accompanied by a
change in the way you specify the initial layout and geometry in
app-defaults/Xpp. See the CHANGES file for more details.
c) z_%forall%_intro_conv1 and z_%exists%_intro_conv1 no longer fail if bound
variables declared by schemas-as-declarations had been renamed. Instead they
introduce schema renamings as necessary to convert the declarations back into
valid Z. This fixes a bug reported by Phil Clayton whereby stripping either
failed or produced a result that was not fully simplified.
My thanks to everyone who has helped with this release and my apologies to
anyone who contributed requests for features that haven't been implemented yet.
Your requests are much appreciated and are on the to-do list.
Proofpower mailing list