--- a/src/HOL/Finite_Set.thy Fri Aug 13 10:38:28 2010 +0200 +++ b/src/HOL/Finite_Set.thy Fri Aug 13 10:51:23 2010 +0200 @@ -6,7 +6,7 @@ header {* Finite sets *} theory Finite_Set -imports Power Option +imports Option Power begin subsection {* Predicate for finite sets *}