equal
deleted
inserted
replaced
119 lordered_ab_group_add_meet ~> semilattice_inf_ab_group_add |
119 lordered_ab_group_add_meet ~> semilattice_inf_ab_group_add |
120 lordered_ab_group_add_join ~> semilattice_sup_ab_group_add |
120 lordered_ab_group_add_join ~> semilattice_sup_ab_group_add |
121 lordered_ring ~> lattice_ring |
121 lordered_ring ~> lattice_ring |
122 |
122 |
123 INCOMPATIBILITY. |
123 INCOMPATIBILITY. |
124 |
|
125 * New theory Algebras contains generic algebraic structures and |
|
126 generic algebraic operations. |
|
127 |
124 |
128 * HOLogic.strip_psplit: types are returned in syntactic order, similar |
125 * HOLogic.strip_psplit: types are returned in syntactic order, similar |
129 to other strip and tuple operations. INCOMPATIBILITY. |
126 to other strip and tuple operations. INCOMPATIBILITY. |
130 |
127 |
131 * Various old-style primrec specifications in the HOL theories have been |
128 * Various old-style primrec specifications in the HOL theories have been |