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