src/HOL/Cardinals/Wellorder_Embedding.thy

--- a/src/HOL/Cardinals/Wellorder_Embedding.thy	Wed Jan 22 09:45:30 2014 +0100
+++ b/src/HOL/Cardinals/Wellorder_Embedding.thy	Wed Jan 22 10:13:40 2014 +0100
@@ -103,7 +103,7 @@
 using one_set_greater[of UNIV UNIV] by auto
 
 
-subsection {* Uniqueness of embeddings  *}
+subsection {* Uniqueness of embeddings *}
 
 lemma comp_embedS:
 assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"