summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Cardinals/Cardinal_Order_Relation.thy

changeset 54989 | 0fd6b0660242 |

parent 54980 | 7e0573a490ee |

child 55023 | 38db7814481d |

--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy Sat Jan 11 08:10:14 2014 +0100 +++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy Sat Jan 11 21:03:11 2014 +0100 @@ -1854,7 +1854,7 @@ text{* Below, the type of "A" is not important -- we just had to choose an appropriate type to make "A" possible. What is important is that arbitrarily large - \<not>finite sets of stable cardinality exist. *} + infinite sets of stable cardinality exist. *} lemma infinite_stable_exists: assumes CARD: "\<forall>r \<in> R. Card_order (r::'a rel)"