summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Sat, 11 Jan 2014 21:03:11 +0100 | |

changeset 54989 | 0fd6b0660242 |

parent 54988 | f3b6f80cc15d |

child 55002 | 81fff1c65943 |

shot in the dark to make LaTeX happy again

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