--- 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