equal
deleted
inserted
replaced
150 targets and in any nested target built on top of a target supporting |
150 targets and in any nested target built on top of a target supporting |
151 "global_interpretation". |
151 "global_interpretation". |
152 |
152 |
153 |
153 |
154 *** HOL *** |
154 *** HOL *** |
|
155 |
|
156 * New order prover. |
155 |
157 |
156 * Theorems "antisym" and "eq_iff" in class "order" have been renamed to |
158 * Theorems "antisym" and "eq_iff" in class "order" have been renamed to |
157 "order.antisym" and "order.eq_iff", to coexist locally with "antisym" |
159 "order.antisym" and "order.eq_iff", to coexist locally with "antisym" |
158 and "eq_iff" from locale "ordering". INCOMPATIBILITY: significant |
160 and "eq_iff" from locale "ordering". INCOMPATIBILITY: significant |
159 potential for change can be avoided if interpretations of type class |
161 potential for change can be avoided if interpretations of type class |