summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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| )"