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:
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
