src/ZF/Ordinal.thy

--- a/src/ZF/Ordinal.thy	Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/Ordinal.thy	Mon Dec 07 10:23:50 2015 +0100
@@ -390,7 +390,7 @@
 by (rule_tac i = i and j = j in Ord_linear2, auto)
 
 
-subsubsection \<open>Some Rewrite Rules for @{text "<"}, @{text "\<le>"}\<close>
+subsubsection \<open>Some Rewrite Rules for \<open><\<close>, \<open>\<le>\<close>\<close>
 
 lemma Ord_mem_iff_lt: "Ord(j) ==> i\<in>j <-> i<j"
 by (unfold lt_def, blast)