| changeset 66435 | 292680dde314 |
| parent 65964 | 3de7464450b0 |
| child 67386 | 998e01d6f8fd |
--- 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}\\