| changeset 21409 | 6aa28caa96c5 |
| parent 21404 | eb85850d3eb7 |
| child 21575 | 89463ae2612d |
--- a/src/HOL/Finite_Set.thy Sat Nov 18 00:20:15 2006 +0100 +++ b/src/HOL/Finite_Set.thy Sat Nov 18 00:20:16 2006 +0100 @@ -7,7 +7,7 @@ header {* Finite sets *} theory Finite_Set -imports Power Inductive Lattices +imports Power Divides Inductive Lattices begin subsection {* Definition and basic properties *}