# HG changeset patch
# User wenzelm
# Date 1444590188 -7200
# Node ID 520a282941682b694ed78beda6cf07a4be2ffff8
# Parent  4d9c716e7786e901972fd022969914a1caa21b18
proper document source;

diff -r 4d9c716e7786 -r 520a28294168 src/ZF/Ordinal.thy
--- 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)