equal
deleted
inserted
replaced
262 |
262 |
263 * Discontinued theories Code_Integer and Efficient_Nat by a more |
263 * Discontinued theories Code_Integer and Efficient_Nat by a more |
264 fine-grain stack of theories Code_Target_Int, Code_Binary_Nat, |
264 fine-grain stack of theories Code_Target_Int, Code_Binary_Nat, |
265 Code_Target_Nat and Code_Target_Numeral. See the tutorial on code |
265 Code_Target_Nat and Code_Target_Numeral. See the tutorial on code |
266 generation for details. INCOMPATIBILITY. |
266 generation for details. INCOMPATIBILITY. |
|
267 |
|
268 * Complete_Partial_Order.admissible is defined outside the type |
|
269 class ccpo, but with mandatory prefix ccpo. Admissibility theorems |
|
270 lose the class predicate assumption or sort constraint when possible. |
|
271 INCOMPATIBILITY. |
267 |
272 |
268 * Introduce type class "conditionally_complete_lattice": Like a |
273 * Introduce type class "conditionally_complete_lattice": Like a |
269 complete lattice but does not assume the existence of the top and |
274 complete lattice but does not assume the existence of the top and |
270 bottom elements. Allows to generalize some lemmas about reals and |
275 bottom elements. Allows to generalize some lemmas about reals and |
271 extended reals. Removed SupInf and replaced it by the instantiation |
276 extended reals. Removed SupInf and replaced it by the instantiation |