changeset 76522 | 3fc92362fbb5 |
parent 76521 | 15f868460de9 |
child 76559 | 4352d0ff165a |
--- a/NEWS Mon Nov 21 13:48:58 2022 +0100 +++ b/NEWS Mon Nov 21 13:53:04 2022 +0100 @@ -26,8 +26,9 @@ Minor INCOMPATIBILITY. * Theory "HOL.Relation": - - Strengthened lemmas. Minor INCOMPATIBILITY. + - Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY. total_on_singleton + reflp_equality[simp] ~> reflp_on_equality[simp] - Added lemmas. antisym_if_asymp antisymp_if_asymp