--- 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":