--- a/src/ZF/Constructible/Wellorderings.thy Fri Jan 04 21:49:06 2019 +0100
+++ b/src/ZF/Constructible/Wellorderings.thy Fri Jan 04 23:22:53 2019 +0100
@@ -6,7 +6,7 @@
theory Wellorderings imports Relative begin
-text\<open>We define functions analogous to @{term ordermap} @{term ordertype}
+text\<open>We define functions analogous to \<^term>\<open>ordermap\<close> \<^term>\<open>ordertype\<close>
but without using recursion. Instead, there is a direct appeal
to Replacement. This will be the basis for a version relativized
to some class \<open>M\<close>. The main result is Theorem I 7.6 in Kunen,