equal
deleted
inserted
replaced
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 |
12 |
13 *** HOL *** |
13 *** HOL *** |
|
14 |
|
15 * HOLogic.strip_psplit: types are returned in syntactic order, similar |
|
16 to other strip and tuple operations. INCOMPATIBILITY. |
14 |
17 |
15 * Various old-style primrec specifications in the HOL theories have been |
18 * Various old-style primrec specifications in the HOL theories have been |
16 replaced by new-style primrec, especially in theory List. The corresponding |
19 replaced by new-style primrec, especially in theory List. The corresponding |
17 constants now have authentic syntax. INCOMPATIBILITY. |
20 constants now have authentic syntax. INCOMPATIBILITY. |
18 |
21 |