changeset 76496 | 855b5f0456d8 |
parent 76495 | a718547c3493 |
child 76497 | ebcfaddd3cb6 |
--- a/NEWS Wed Nov 09 16:45:12 2022 +0100 +++ b/NEWS Wed Nov 09 16:39:45 2022 +0100 @@ -50,6 +50,8 @@ * Theory "HOL.Transitive_Closure": - Strengthened lemma reflp_rtranclp and renamed to reflp_on_rtranclp. Minor INCOMPATIBILITY. + - Added lemmas. + reflp_on_reflclp[simp] * Theory "HOL.Wellfounded": - Added lemmas.