changeset 76495 | a718547c3493 |
parent 76478 | d84568379f3f |
child 76496 | 855b5f0456d8 |
--- a/NEWS Tue Nov 08 08:41:48 2022 +0100 +++ b/NEWS Wed Nov 09 16:45:12 2022 +0100 @@ -47,6 +47,10 @@ preorder.reflp_le[simp] totalp_on_singleton[simp] +* Theory "HOL.Transitive_Closure": + - Strengthened lemma reflp_rtranclp and renamed to reflp_on_rtranclp. + Minor INCOMPATIBILITY. + * Theory "HOL.Wellfounded": - Added lemmas. wfP_if_convertible_to_nat