| changeset 21249 | d594c58e24ed |
| parent 21215 | 7c9337a0e30a |
| child 21404 | eb85850d3eb7 |
--- a/src/HOL/Finite_Set.thy Wed Nov 08 19:46:10 2006 +0100 +++ b/src/HOL/Finite_Set.thy Wed Nov 08 19:48:34 2006 +0100 @@ -7,7 +7,7 @@ header {* Finite sets *} theory Finite_Set -imports Power Inductive Lattice_Locales +imports Power Inductive Lattices begin subsection {* Definition and basic properties *}