diff -r e324f8918c98 -r d63776c3be97 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Fri Mar 14 19:57:12 2008 +0100
+++ b/src/HOL/Library/Library.thy	Fri Mar 14 19:57:32 2008 +0100
@@ -33,6 +33,7 @@
   Numeral_Type
   OptionalSugar
   Option_ord
+  Order_Relation
   Parity
   Permutation
   Primes