From 1253e33fc97a9b4a28a55fc8b924787228823128 Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Fri, 31 May 2024 14:16:11 +1000 Subject: [PATCH] =?UTF-8?q?Use=20correct=20Hungarian=20accent=20in=20K?= =?UTF-8?q?=C5=91nig=20Lemma=20comment?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit My googling suggests that oe is an acceptable ASCII-only rendering of this so keeping the theorem names as koenig_lemma etc is reasonable. --- src/pred_set/src/pred_setScript.sml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/pred_set/src/pred_setScript.sml b/src/pred_set/src/pred_setScript.sml index 58dccd78c2..ca42fce419 100644 --- a/src/pred_set/src/pred_setScript.sml +++ b/src/pred_set/src/pred_setScript.sml @@ -7531,7 +7531,7 @@ Proof QED (* ---------------------------------------------------------------------- - A proof of Koenig's Lemma + A proof of Kőnig's Lemma UOK ---------------------------------------------------------------------- *) (* a counting exercise for R-trees. If x0 has finitely many successors, and