src/HOL/Finite_Set.thy
changeset 16760 5c5f051aaaaa
parent 16733 236dfafbeb63
child 16775 c1b87ef4a1c3
     1.1 --- a/src/HOL/Finite_Set.thy	Fri Jul 08 11:37:53 2005 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Fri Jul 08 11:38:30 2005 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  header {* Finite sets *}
     1.5  
     1.6  theory Finite_Set
     1.7 -imports Divides Power Inductive Lattice_Locales
     1.8 +imports Power Inductive Lattice_Locales
     1.9  begin
    1.10  
    1.11  subsection {* Definition and basic properties *}