diff -r dbf61e36f8e9 -r 3150eba724a1 src/HOL/Finite.thy
--- a/src/HOL/Finite.thy	Mon Jun 02 12:19:01 1997 +0200
+++ b/src/HOL/Finite.thy	Tue Jun 03 10:53:58 1997 +0200
@@ -6,7 +6,7 @@
 Finite sets and their cardinality
 *)
 
-Finite = Divides +
+Finite = Divides + Power + 
 
 consts Fin :: 'a set => 'a set set