1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Note: this file isn't used anymore. Incompatibilities are documented
as part of CHANGES.
Incompatibilities beyond 8.4...
- Syntax: "x -> y" has now lower priority than "<->" "A -> B <-> C" is
now "A -> (B <-> C)"
- Tactics: tauto and intuition no longer accidentally destruct binary
connectives or records other than and, or, prod, sum, iff. In most
of cases, dtauto or dintuition, though stronger than 8.3 tauto and
8.3 intuition will provide compatibility.
- "Solve Obligations using" is now "Solve Obligations with".
|
