# HG changeset patch
# User haftmann
# Date 1389470591 -3600
# Node ID 0fd6b06602420731a4d31d2fbe3d80d301ce1f8f
# Parent f3b6f80cc15d24a0680eec607d5420c91037a769
shot in the dark to make LaTeX happy again
diff -r f3b6f80cc15d -r 0fd6b0660242 src/HOL/Cardinals/Cardinal_Order_Relation.thy
--- 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
- \finite sets of stable cardinality exist. *}
+ infinite sets of stable cardinality exist. *}
lemma infinite_stable_exists:
assumes CARD: "\r \ R. Card_order (r::'a rel)"