src/Doc/Main/Main_Doc.thy
changeset 65956 639eb3617a86
parent 65954 431024edc9cf
child 65964 3de7464450b0
--- a/src/Doc/Main/Main_Doc.thy	Sun May 28 15:46:26 2017 +0200
+++ b/src/Doc/Main/Main_Doc.thy	Mon May 29 09:14:15 2017 +0200
@@ -552,6 +552,7 @@
 @{const List.map} & @{typeof List.map}\\
 @{const List.measures} & @{term_type_only List.measures "('a\<Rightarrow>nat)list\<Rightarrow>('a*'a)set"}\\
 @{const List.nth} & @{typeof List.nth}\\
+@{const List.nths} & @{typeof List.nths}\\
 @{const List.remdups} & @{typeof List.remdups}\\
 @{const List.removeAll} & @{typeof List.removeAll}\\
 @{const List.remove1} & @{typeof List.remove1}\\
@@ -560,10 +561,10 @@
 @{const List.rotate} & @{typeof List.rotate}\\
 @{const List.rotate1} & @{typeof List.rotate1}\\
 @{const List.set} & @{term_type_only List.set "'a list \<Rightarrow> 'a set"}\\
+@{const List.shuffle} & @{typeof List.shuffle}\\
 @{const List.sort} & @{typeof List.sort}\\
 @{const List.sorted} & @{typeof List.sorted}\\
 @{const List.splice} & @{typeof List.splice}\\
-@{const List.sublist} & @{typeof List.sublist}\\
 @{const List.take} & @{typeof List.take}\\
 @{const List.takeWhile} & @{typeof List.takeWhile}\\
 @{const List.tl} & @{typeof List.tl}\\
@@ -656,4 +657,4 @@
 \<close>
 (*<*)
 end
-(*>*)
\ No newline at end of file
+(*>*)