equal
deleted
inserted
replaced
5 ---------------------------- |
5 ---------------------------- |
6 |
6 |
7 *** Overview of INCOMPATIBILITIES (see below for more details) *** |
7 *** Overview of INCOMPATIBILITIES (see below for more details) *** |
8 |
8 |
9 * HOL: the constant for f``x is now "image" rather than "op ``". |
9 * HOL: the constant for f``x is now "image" rather than "op ``". |
|
10 |
|
11 * HOL: the cartesian product is now "<*>" instead of "Times". |
|
12 the lexicographic product is now "<*lex*>" instead of "**". |
10 |
13 |
11 * HOL: exhaust_tac on datatypes superceded by new generic case_tac; |
14 * HOL: exhaust_tac on datatypes superceded by new generic case_tac; |
12 |
15 |
13 * HOL: simplification no longer dives into case-expressions |
16 * HOL: simplification no longer dives into case-expressions |
14 |
17 |