diff -r 507e519a0dad -r c84af7f39a6b src/HOL/Set.thy --- a/src/HOL/Set.thy Tue Sep 20 13:58:58 2005 +0200 +++ b/src/HOL/Set.thy Tue Sep 20 14:03:37 2005 +0200 @@ -6,7 +6,7 @@ header {* Set theory for higher-order logic *} theory Set -imports Orderings +imports LOrder begin text {* A set in HOL is simply a predicate. *}