--- a/src/HOL/Library/Library.thy Fri Mar 07 13:53:00 2008 +0100 +++ b/src/HOL/Library/Library.thy Fri Mar 07 13:53:01 2008 +0100 @@ -32,6 +32,7 @@ Nested_Environment Numeral_Type OptionalSugar + Option_ord Parity Permutation Primes