Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
finite type class instance for `set`
authorhaftmann
Sat, 24 Dec 2011 15:53:08 +0100
changeset 45962 fc77947a7db4
parent 45961 5cefe17916a6
child 45963 1c7e6454883e
finite type class instance for `set`
src/HOL/Finite_Set.thy file | annotate | diff | comparison | revisions 
--- 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)
isabelle