# HG changeset patch
# User desharna
# Date 1654351164 -7200
# Node ID a7c6722fbaf1769a379af9ebfdda2a8841a93e48
# Parent  75e1b94396c6d63ed7d163548831cff7957bb471
NEWS

diff -r 75e1b94396c6 -r a7c6722fbaf1 NEWS
--- a/NEWS	Sat Jun 04 16:00:14 2022 +0200
+++ b/NEWS	Sat Jun 04 15:59:24 2022 +0200
@@ -44,6 +44,7 @@
   - Added predicate reflp_on and redefined reflp to ab an abbreviation.
     Lemma reflp_def is explicitly provided for backward compatibility
     but its usage is discouraged. Minor INCOMPATIBILITY.
+  - Added predicate totalp_on and abbreviation totalp.
   - Added lemmas.
       preorder.asymp_greater
       preorder.asymp_less
@@ -51,6 +52,10 @@
       reflp_onI
       reflp_on_subset
       total_on_subset
+      totalpD
+      totalpI
+      totalp_onD
+      totalp_onI
       totalp_on_subset
 
 * Theory "HOL-Library.Multiset":