Dear All,

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

Reply via email to