| changeset 35029 | 22aab1c5e5a8 |
| parent 35027 | ed7d12bcf8f8 |
| child 35030 | f2f1e50bf65d |
| 35028:108662d50512 | 35029:22aab1c5e5a8 |
|---|---|
57 ordered_semiring_1 ~> linordered_semiring_1 |
57 ordered_semiring_1 ~> linordered_semiring_1 |
58 ordered_semiring_1_strict ~> linordered_semiring_1_strict |
58 ordered_semiring_1_strict ~> linordered_semiring_1_strict |
59 ordered_semiring_strict ~> linordered_semiring_strict |
59 ordered_semiring_strict ~> linordered_semiring_strict |
60 |
60 |
61 INCOMPATIBILITY. |
61 INCOMPATIBILITY. |
62 |
|
63 * Index syntax for structures must be imported explicitly from library |
|
64 theory Structure_Syntax. INCOMPATIBILITY. |
|
62 |
65 |
63 * new theory Algebras.thy contains generic algebraic structures and |
66 * new theory Algebras.thy contains generic algebraic structures and |
64 generic algebraic operations. INCOMPATIBILTY: constants zero, one, |
67 generic algebraic operations. INCOMPATIBILTY: constants zero, one, |
65 plus, minus, uminus, times, inverse, divide, abs, sgn, less_eq and less |
68 plus, minus, uminus, times, inverse, divide, abs, sgn, less_eq and less |
66 have been moved from HOL.thy to Algebras.thy. |
69 have been moved from HOL.thy to Algebras.thy. |