diff -r e911be103066 -r 81cc8f2ea9e7 NEWS --- a/NEWS Mon Nov 01 15:24:53 2021 +0100 +++ b/NEWS Mon Nov 01 15:49:03 2021 +0100 @@ -153,6 +153,8 @@ *** HOL *** +* New order prover. + * Theorems "antisym" and "eq_iff" in class "order" have been renamed to "order.antisym" and "order.eq_iff", to coexist locally with "antisym" and "eq_iff" from locale "ordering". INCOMPATIBILITY: significant