author | Lukas Stevens <mail@lukas-stevens.de> |
Fri, 22 Jul 2022 14:21:53 +0000 | |
changeset 75670 | acf86c9f7698 |
parent 75669 | 43f5dfb7fa35 |
child 75690 | fc4eaa10ec77 |
--- 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"