# HG changeset patch
# User nipkow
# Date 1502828596 -7200
# Node ID 292680dde31447623a1b5a1fe27a5f938a4ea638
# Parent  5d7e770c7d5d3ea742d3ed1fb3698694bc27f43d
NEWS sorted_wrt

diff -r 5d7e770c7d5d -r 292680dde314 NEWS
--- a/NEWS	Tue Aug 15 19:47:08 2017 +0200
+++ b/NEWS	Tue Aug 15 22:23:16 2017 +0200
@@ -131,8 +131,11 @@
 
 * Material on infinite products in HOL-Analysis
 
-* "sublist" from theory List renamed to "nths" in analogy with "nth".
-"sublisteq" renamed to "subseq".  Minor INCOMPATIBILITY.
+* Theory List:
+  "sublist" renamed to "nths" in analogy with "nth".
+  "sublisteq" renamed to "subseq".
+  Minor INCOMPATIBILITY.
+  New generic function "sorted_wrt"
 
 * Theories "GCD" and "Binomial" are already included in "Main" (instead
 of "Complex_Main").
diff -r 5d7e770c7d5d -r 292680dde314 src/Doc/Main/Main_Doc.thy
--- a/src/Doc/Main/Main_Doc.thy	Tue Aug 15 19:47:08 2017 +0200
+++ b/src/Doc/Main/Main_Doc.thy	Tue Aug 15 22:23:16 2017 +0200
@@ -563,6 +563,7 @@
 @{const List.shuffle} & @{typeof List.shuffle}\\
 @{const List.sort} & @{typeof List.sort}\\
 @{const List.sorted} & @{typeof List.sorted}\\
+@{const List.sorted_wrt} & @{typeof List.sorted_wrt}\\
 @{const List.splice} & @{typeof List.splice}\\
 @{const List.take} & @{typeof List.take}\\
 @{const List.takeWhile} & @{typeof List.takeWhile}\\