# HG changeset patch
# User Lukas Stevens <mail@lukas-stevens.de>
# Date 1658499713 0
# Node ID acf86c9f769846a503544f425085112bbc54cbe8
# Parent  43f5dfb7fa35b9f301072c8f3d844daab7a7a096
fix document build error

diff -r 43f5dfb7fa35 -r acf86c9f7698 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri Jul 22 14:39:56 2022 +0200
+++ b/src/HOL/Orderings.thy	Fri Jul 22 14:21:53 2022 +0000
@@ -975,7 +975,7 @@
   trans
 
 text \<open>These support proving chains of decreasing inequalities
-    a \<ge> b \<ge> c ... in Isar proofs.\<close>
+    a \<open>\<ge>\<close> b \<open>\<ge>\<close> c ... in Isar proofs.\<close>
 
 lemma xt1 [no_atp]:
   "a = b \<Longrightarrow> b > c \<Longrightarrow> a > c"