--- 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").
--- 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}\\