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