src/HOL/BNF/Countable_Type.thy
changeset 52660 7f7311d04727
parent 52659 58b87aa4dc3b
child 52662 c7cae5ce217d
     1.1 --- a/src/HOL/BNF/Countable_Type.thy	Mon Jul 15 14:23:51 2013 +0200
     1.2 +++ b/src/HOL/BNF/Countable_Type.thy	Mon Jul 15 15:50:39 2013 +0200
     1.3 @@ -53,16 +53,6 @@
     1.4  shows "countable A"
     1.5  using countable_ordLeq[OF ordLess_imp_ordLeq[OF AB] B] .
     1.6  
     1.7 -lemma ordLeq_countable:
     1.8 -assumes "|A| \<le>o |B|" and "countable B"
     1.9 -shows "countable A"
    1.10 -using assms unfolding countable_card_of_nat by(rule ordLeq_transitive)
    1.11 -
    1.12 -lemma ordLess_countable:
    1.13 -assumes A: "|A| <o |B|" and B: "countable B"
    1.14 -shows "countable A"
    1.15 -by (rule ordLeq_countable[OF ordLess_imp_ordLeq[OF A] B])
    1.16 -
    1.17  subsection{*  The type of countable sets *}
    1.18  
    1.19  typedef 'a cset = "{A :: 'a set. countable A}"