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:

## Advertising

http://www.lemma-one.com/ProofPower/getting/experimental/OpenProofPower-2.9.1w2.rda.110727.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 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] induction_thm; 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 it. 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. Regards, Rob.

_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com