# HG changeset patch
# User huffman
# Date 1214936808 -7200
# Node ID 1e25ac05cd871ef628a49c43f8d528a3cefffa61
# Parent  510eed16fab56fd4563e934a30583ef6311ec88c
prove lemma finite in context of finite class

diff -r 510eed16fab5 -r 1e25ac05cd87 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Jul 01 20:10:59 2008 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Jul 01 20:26:48 2008 +0200
@@ -429,9 +429,14 @@
 setup {* Sign.parent_path *}
 hide const finite
 
-lemma finite [simp]: "finite (A \<Colon> 'a\<Colon>finite set)"
+context finite
+begin
+
+lemma finite [simp]: "finite (A \<Colon> 'a set)"
   by (rule subset_UNIV finite_UNIV finite_subset)+
 
+end
+
 lemma UNIV_unit [noatp]:
   "UNIV = {()}" by auto