--- a/src/HOL/Finite_Set.thy Thu Nov 28 15:44:34 2002 +0100
+++ b/src/HOL/Finite_Set.thy Fri Nov 29 09:48:28 2002 +0100
@@ -11,20 +11,23 @@
subsection {* Collection of finite sets *}
consts Finites :: "'a set set"
+syntax
+ finite :: "'a set => bool"
+translations
+ "finite A" == "A : Finites"
inductive Finites
intros
emptyI [simp, intro!]: "{} : Finites"
insertI [simp, intro!]: "A : Finites ==> insert a A : Finites"
-syntax
- finite :: "'a set => bool"
-translations
- "finite A" == "A : Finites"
-
axclass finite \<subseteq> type
finite: "finite UNIV"
+lemma ex_new_if_finite: -- "does not depend on def of finite at all"
+ "\<lbrakk> ~finite(UNIV::'a set); finite A \<rbrakk> \<Longrightarrow> \<exists>a::'a. a ~: A"
+by(subgoal_tac "A ~= UNIV", blast, blast)
+
lemma finite_induct [case_names empty insert, induct set: Finites]:
"finite F ==>