# 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 \ i" by (rule_tac i = i and j = j in Ord_linear2, auto) -subsubsection\Some Rewrite Rules for <, \\ + +subsubsection \Some Rewrite Rules for @{text "<"}, @{text "\"}\ lemma Ord_mem_iff_lt: "Ord(j) ==> i\j <-> i