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 * new theory Algebras.thy contains generic algebraic structures and |
|
16 generic algebraic operations. INCOMPATIBILTY: constants zero, one, |
|
17 plus, minus, uminus, times, inverse, divide, abs, sgn, less_eq and less |
|
18 have been moved from HOL.thy to Algebras.thy. |
14 |
19 |
15 * HOLogic.strip_psplit: types are returned in syntactic order, similar |
20 * HOLogic.strip_psplit: types are returned in syntactic order, similar |
16 to other strip and tuple operations. INCOMPATIBILITY. |
21 to other strip and tuple operations. INCOMPATIBILITY. |
17 |
22 |
18 * Various old-style primrec specifications in the HOL theories have been |
23 * Various old-style primrec specifications in the HOL theories have been |