New features and changes since 2.2
==================================

(1) The search command can now take a depth bound.

(2) There is a new descent function metaNormalize that puts a term in
theory normal form without doing any rewrites.

(3) The builtin MACHINE-INT module is now available.

(4) Owing to fears about the unsoundness of _==_ in the presence of
non-confluence and related issues a number of features have been
modified, replaced or removed altogether.
- fmod IDENTICAL is expunged due to alleged unsoundness.
- The lazy sort test operators _:::s have likewise disappeared.

(5) TAO-SET is now replaced by two notions of an order relation:
STRICT-WEAK-ORDER (transitive, irreflexive, incomparability transitive),
and TOTAL-PREORDER (transitive, reflexive, total)

(6) There are now two versions of sortable lists with these orderings:
WEAKLY-SORTABLE-LIST uses STRICT-WEAK-ORDER and WEAKLY-SORTABLE-LIST'
uses TOTAL-PREORDER. Both provide a stable sort() operator.

(7) There are two further notions of linear ordering: STRICT-TOTAL-ORDER
adds totality to STRICT-WEAK-ORDER and TOTAL-ORDER adds antisymmetry to
TOTAL-PREORDER; and there are two versions of sortable lists with these
orderings: SORTABLE-LIST uses STRICT-TOTAL-ORDER and SORTABLE-LIST'
uses TOTAL-ORDER. Since these use linear orderings, the issue of
stability does not arise.

(8) Two sets of view are provided for the standard built in data types;
views such as NAT< map from STRICT-TOTAL-ORDER while views such as
NAT<= map from TOTAL-ORDER.

(9) makeList() in LIST-AND-SET was non-confluent both because no order
was specified for putting the elements in the list, and because due to
idempotence on sets, the same element could be placed in the list more
than once. This is fixed by reimplementing makeList() in two new
modules, SORTABLE-LIST-AND-SET which requires a STRICT-TOTAL-ORDER and
SORTABLE-LIST-AND-SET' which requires a TOTAL-ORDER. The availability
of a linear order allows the resulting list to be unambiguous.

(10) min/max operators in FLOAT.

(11) Metalevel projection functions now support parameterized metamodules.

(12) erwrite supports limit and continue.

(13) Subset tests for SET and SET*.

(14) Predefined term ordering module in term-order.maude.