# HG changeset patch # User wenzelm # Date 1369686748 -7200 # Node ID fce4a365f2804b327ee072fb0f8b52f33842ae42 # Parent 636b62eb7e88d8bdf5632faa11e726a284077d7d actually test theory Order_Union; 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