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