# HG changeset patch
# User haftmann
# Date 1324738388 -3600
# Node ID fc77947a7db45f842bf61ad43872449c8d4f1367
# Parent  5cefe17916a6f4cbfb13fc01bf99fe75adda3a07
finite type class instance for `set`

diff -r 5cefe17916a6 -r fc77947a7db4 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sat Dec 24 15:53:08 2011 +0100
+++ b/src/HOL/Finite_Set.thy	Sat Dec 24 15:53:08 2011 +0100
@@ -509,6 +509,9 @@
 instance bool :: finite proof
 qed (simp add: UNIV_bool)
 
+instance set :: (finite) finite
+  by default (simp only: Pow_UNIV [symmetric] finite_Pow_iff finite)
+
 instance unit :: finite proof
 qed (simp add: UNIV_unit)