src/HOL/BNF_Cardinal_Order_Relation.thy
changeset 58623 2db1df2c8467
parent 58127 b7cab82f488e
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Tue Oct 07 23:12:08 2014 +0200
     1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Tue Oct 07 23:29:43 2014 +0200
     1.3 @@ -826,7 +826,7 @@
     1.4  theorem @{text "Card_order_Times_same_infinite"}, which states that self-product
     1.5  does not increase cardinality -- the proof of this fact adapts a standard
     1.6  set-theoretic argument, as presented, e.g., in the proof of theorem 1.5.11
     1.7 -at page 47 in \cite{card-book}. Then everything else follows fairly easily. *}
     1.8 +at page 47 in @{cite "card-book"}. Then everything else follows fairly easily. *}
     1.9  
    1.10  lemma infinite_iff_card_of_nat:
    1.11  "\<not> finite A \<longleftrightarrow> ( |UNIV::nat set| \<le>o |A| )"