# HG changeset patch
# User nipkow
# Date 1538557748 -7200
# Node ID e2780bb2639537beb940bb0878d364670357ac89
# Parent  c2de7a5c8de95ef485d11ccd87fc3e5655aebcd8
shuffle -> shuffles

diff -r c2de7a5c8de9 -r e2780bb26395 src/Doc/Main/Main_Doc.thy
--- a/src/Doc/Main/Main_Doc.thy	Wed Oct 03 09:46:42 2018 +0200
+++ b/src/Doc/Main/Main_Doc.thy	Wed Oct 03 11:09:08 2018 +0200
@@ -552,7 +552,7 @@
 @{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.shuffles} & @{typeof List.shuffles}\\
 @{const List.sort} & @{typeof List.sort}\\
 @{const List.sorted} & @{typeof List.sorted}\\
 @{const List.sorted_wrt} & @{typeof List.sorted_wrt}\\