src/HOL/Finite_Set.thy
changeset 15131 c69542757a4d
parent 15124 1d9b4fcd222d
child 15140 322485b816ac
--- a/src/HOL/Finite_Set.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Finite_Set.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,7 +6,9 @@
 
 header {* Finite sets *}
 
-theory Finite_Set = Divides + Power + Inductive:
+theory Finite_Set
+import Divides Power Inductive
+begin
 
 subsection {* Collection of finite sets *}