Dear All,

It has taken a little bit longer than I would have hoped but 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.110226 are:

a) Rewriting with higher-order matching is now supported in HOL. It is enabled 
using the component proof context "'sho_rw"
(short for: "simple higher-order rewriting"). As an example, higher-order 
rewriting with the theorem prenex_clauses will put a formula in prenex normal 
form. See if the following turns you into an intuitionist:

    merge_pcs_rule1 ["predicates", "'sho_rw"] rewrite_rule[prenex_clauses] 

b) Thanks to Phil Clayton, ProofPower-Z now supports empty declaration parts in 
paragraphs (as well as in expressions
which were already supported, also thanks to Phil, in 2.9.1w2.rda.110226).

c) The guillemet brackets that are used in Spivey Z and ISO Standard Z around 
the domains of the constructors in a free type definition are now supported in 
ProofPower-Z. These brackets are entered as %<<% and %>>% and are typeset as in 
the Z Reference Manual or the ISO Standard LaTeX mark-up. The brackets are 
defined as an outfix operator in the toolkit with defining property %<<% x %>>% 
= x. So you can use them as a general purpose form of brackets that are not 
eliminated automatically by the parser.

d) You can now use == as an alternative to %def% in abbreviation definitions 
and binding displays in ProofPower-Z.

e) There are new underlining bracket characters in the font. These appear on 
screen as underlined brackets and cause the text they enclose to be underlined 
when typeset.

f) A new operator is defined in ProofPower-Z whose name is "_ %ulbegin% _ 
%ulend% _" (where %ulbegin% and %ulend% are the ASCII names for the underlining 
bracket characters - so this typesets as three underscores with the middle one 
underlined). It is defined so that "x %ulbegin% R %ulend% y" holds iff (x, y) 
is a member of the relation R. This effectively generalises the feature in 
Spivey Z whereby underlined identifiers act as infix relation symbols. In 
ProofPower-Z you can now use any expression as an infix relation by underlining 

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