NEWS sorted_wrt
authornipkow
Tue Aug 15 22:23:16 2017 +0200 (21 months ago)
changeset 66435292680dde314
parent 66434 5d7e770c7d5d
child 66436 36a01c02d0ca
NEWS sorted_wrt
NEWS
src/Doc/Main/Main_Doc.thy
     1.1 --- a/NEWS	Tue Aug 15 19:47:08 2017 +0200
     1.2 +++ b/NEWS	Tue Aug 15 22:23:16 2017 +0200
     1.3 @@ -131,8 +131,11 @@
     1.4  
     1.5  * Material on infinite products in HOL-Analysis
     1.6  
     1.7 -* "sublist" from theory List renamed to "nths" in analogy with "nth".
     1.8 -"sublisteq" renamed to "subseq".  Minor INCOMPATIBILITY.
     1.9 +* Theory List:
    1.10 +  "sublist" renamed to "nths" in analogy with "nth".
    1.11 +  "sublisteq" renamed to "subseq".
    1.12 +  Minor INCOMPATIBILITY.
    1.13 +  New generic function "sorted_wrt"
    1.14  
    1.15  * Theories "GCD" and "Binomial" are already included in "Main" (instead
    1.16  of "Complex_Main").
     2.1 --- a/src/Doc/Main/Main_Doc.thy	Tue Aug 15 19:47:08 2017 +0200
     2.2 +++ b/src/Doc/Main/Main_Doc.thy	Tue Aug 15 22:23:16 2017 +0200
     2.3 @@ -563,6 +563,7 @@
     2.4  @{const List.shuffle} & @{typeof List.shuffle}\\
     2.5  @{const List.sort} & @{typeof List.sort}\\
     2.6  @{const List.sorted} & @{typeof List.sorted}\\
     2.7 +@{const List.sorted_wrt} & @{typeof List.sorted_wrt}\\
     2.8  @{const List.splice} & @{typeof List.splice}\\
     2.9  @{const List.take} & @{typeof List.take}\\
    2.10  @{const List.takeWhile} & @{typeof List.takeWhile}\\