src/ZF/Finite.thy
changeset 14883 ca000a495448
parent 13784 b9f6154427a4
child 16417 9bc16273c2d4
     1.1 --- a/src/ZF/Finite.thy	Sun Jun 06 18:36:36 2004 +0200
     1.2 +++ b/src/ZF/Finite.thy	Tue Jun 08 16:22:30 2004 +0200
     1.3 @@ -3,8 +3,6 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1994  University of Cambridge
     1.6  
     1.7 -prove X:Fin(A) ==> |X| < nat
     1.8 -
     1.9  prove:  b: Fin(A) ==> inj(b,b) <= surj(b,b)
    1.10  *)
    1.11  
    1.12 @@ -199,6 +197,17 @@
    1.13   apply (blast dest: FiniteFun_is_fun range_of_fun range_type apply_equality)+
    1.14  done
    1.15  
    1.16 +
    1.17 +subsection{*The Contents of a Singleton Set*}
    1.18 +
    1.19 +constdefs
    1.20 +  contents :: "i=>i"
    1.21 +   "contents(X) == THE x. X = {x}"
    1.22 +
    1.23 +lemma contents_eq [simp]: "contents ({x}) = x"
    1.24 +by (simp add: contents_def)
    1.25 +
    1.26 +
    1.27  ML
    1.28  {*
    1.29  val Fin_intros = thms "Fin.intros";