proper document source;

--- a/src/ZF/Ordinal.thy	Sat Oct 10 22:50:05 2015 +0200
+++ b/src/ZF/Ordinal.thy	Sun Oct 11 21:03:08 2015 +0200
@@ -389,7 +389,8 @@
 lemma not_lt_imp_le: "[| ~ i<j;  Ord(i);  Ord(j) |] ==> j \<le> i"
 by (rule_tac i = i and j = j in Ord_linear2, auto)
 
-subsubsection\<open>Some Rewrite Rules for <, \<le>\<close>
+
+subsubsection \<open>Some Rewrite Rules for @{text "<"}, @{text "\<le>"}\<close>
 
 lemma Ord_mem_iff_lt: "Ord(j) ==> i\<in>j <-> i<j"
 by (unfold lt_def, blast)