diff -r 636b62eb7e88 -r fce4a365f280 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Mon May 27 22:30:07 2013 +0200 +++ b/src/HOL/Library/Library.thy Mon May 27 22:32:28 2013 +0200 @@ -41,6 +41,7 @@ Numeral_Type OptionalSugar Option_ord + Order_Union Parallel Permutation Permutations