equal
deleted
inserted
replaced
8 |
8 |
9 * Code generator: details of internal data cache have no impact on |
9 * Code generator: details of internal data cache have no impact on |
10 the user space functionality any longer. |
10 the user space functionality any longer. |
11 |
11 |
12 * Discontinued unnamed infix syntax (legacy feature for many years) -- |
12 * Discontinued unnamed infix syntax (legacy feature for many years) -- |
13 need to specify constant name and syntax separately. |
13 need to specify constant name and syntax separately. Internal ML |
|
14 datatype constructors have been renamed from InfixName to Infix etc. |
|
15 Minor INCOMPATIBILITY. |
14 |
16 |
15 |
17 |
16 *** HOL *** |
18 *** HOL *** |
17 |
19 |
18 * New set of rules "ac_simps" provides combined assoc / commute rewrites |
20 * New set of rules "ac_simps" provides combined assoc / commute rewrites |