src/ZF/Finite.thy
changeset 24893 b8ef7afe3a6b
parent 16417 9bc16273c2d4
child 26056 6a0801279f4c
     1.1 --- a/src/ZF/Finite.thy	Sun Oct 07 15:49:25 2007 +0200
     1.2 +++ b/src/ZF/Finite.thy	Sun Oct 07 21:19:31 2007 +0200
     1.3 @@ -200,37 +200,11 @@
     1.4  
     1.5  subsection{*The Contents of a Singleton Set*}
     1.6  
     1.7 -constdefs
     1.8 -  contents :: "i=>i"
     1.9 +definition
    1.10 +  contents :: "i=>i"  where
    1.11     "contents(X) == THE x. X = {x}"
    1.12  
    1.13  lemma contents_eq [simp]: "contents ({x}) = x"
    1.14  by (simp add: contents_def)
    1.15  
    1.16 -
    1.17 -ML
    1.18 -{*
    1.19 -val Fin_intros = thms "Fin.intros";
    1.20 -
    1.21 -val Fin_mono = thm "Fin_mono";
    1.22 -val FinD = thm "FinD";
    1.23 -val Fin_induct = thm "Fin_induct";
    1.24 -val Fin_UnI = thm "Fin_UnI";
    1.25 -val Fin_UnionI = thm "Fin_UnionI";
    1.26 -val Fin_subset = thm "Fin_subset";
    1.27 -val Fin_IntI1 = thm "Fin_IntI1";
    1.28 -val Fin_IntI2 = thm "Fin_IntI2";
    1.29 -val Fin_0_induct = thm "Fin_0_induct";
    1.30 -val nat_fun_subset_Fin = thm "nat_fun_subset_Fin";
    1.31 -val FiniteFun_mono = thm "FiniteFun_mono";
    1.32 -val FiniteFun_mono1 = thm "FiniteFun_mono1";
    1.33 -val FiniteFun_is_fun = thm "FiniteFun_is_fun";
    1.34 -val FiniteFun_domain_Fin = thm "FiniteFun_domain_Fin";
    1.35 -val FiniteFun_apply_type = thm "FiniteFun_apply_type";
    1.36 -val FiniteFun_subset = thm "FiniteFun_subset";
    1.37 -val fun_FiniteFunI = thm "fun_FiniteFunI";
    1.38 -val lam_FiniteFun = thm "lam_FiniteFun";
    1.39 -val FiniteFun_Collect_iff = thm "FiniteFun_Collect_iff";
    1.40 -*}
    1.41 -
    1.42  end