src/HOL/BNF_Cardinal_Order_Relation.thy
changeset 63980 f8e556c8ad6f
parent 63040 eb4ddd18d635
child 67091 1393c2340eec
     1.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Sat Oct 01 17:16:35 2016 +0200
     1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Sat Oct 01 17:38:14 2016 +0200
     1.3 @@ -183,7 +183,7 @@
     1.4     card_of_Well_order[of "B"] Field_card_of[of "B"] Field_card_of[of "A"]
     1.5     embed_Field[of "|B|" "|A|" g] by auto
     1.6     obtain h where "bij_betw h A B"
     1.7 -   using * ** 1 Cantor_Bernstein[of f] by fastforce
     1.8 +   using * ** 1 Schroeder_Bernstein[of f] by fastforce
     1.9     hence "|A| =o |B|" using card_of_ordIso by blast
    1.10     hence "|A| \<le>o |B|" using ordIso_iff_ordLeq by auto
    1.11    }