merged

--- a/src/Doc/Nitpick/document/root.tex	Wed Apr 10 11:32:48 2024 +0100
+++ b/src/Doc/Nitpick/document/root.tex	Wed Apr 10 13:23:00 2024 +0200
@@ -28,7 +28,7 @@
 %\def\unk{{?}}
 \def\unk{{\_}}
 \def\unkef{(\lambda x.\; \unk)}
-\def\undef{(\lambda x.\; \_)}
+\def\undefined{(\lambda x.\; \_)}
 %\def\unr{\textit{others}}
 \def\unr{\ldots}
 \def\Abs#1{\hbox{\rm{\guillemetleft}}{\,#1\,}\hbox{\rm{\guillemetright}}}
@@ -368,9 +368,9 @@
 \slshape
 Nitpick found a counterexample for \textit{card} $'a$~= 2 and \textit{card} $'b$~=~1: \\[2\smallskipamount]
 \hbox{}\qquad Free variable: \nopagebreak \\
-\hbox{}\qquad\qquad $f = \undef{}(b_1 := a_1)$ \\
+\hbox{}\qquad\qquad $f = \undefined{}(b_1 := a_1)$ \\
 \hbox{}\qquad Skolem constants: \nopagebreak \\
-\hbox{}\qquad\qquad $g = \undef{}(a_1 := b_1,\> a_2 := b_1)$ \\
+\hbox{}\qquad\qquad $g = \undefined{}(a_1 := b_1,\> a_2 := b_1)$ \\
 \hbox{}\qquad\qquad $y = a_2$
 \postw
 
@@ -390,9 +390,9 @@
 Nitpick found a counterexample for \textit{card} $'a$~= 2: \\[2\smallskipamount]
 \hbox{}\qquad Skolem constant: \nopagebreak \\
 \hbox{}\qquad\qquad $\lambda x.\; f =
-    \undef{}(\!\begin{aligned}[t]
-    & a_1 := \undef{}(a_1 := a_2,\> a_2 := a_1), \\[-2pt]
-    & a_2 := \undef{}(a_1 := a_1,\> a_2 := a_1))\end{aligned}$
+    \undefined{}(\!\begin{aligned}[t]
+    & a_1 := \undefined{}(a_1 := a_2,\> a_2 := a_1), \\[-2pt]
+    & a_2 := \undefined{}(a_1 := a_1,\> a_2 := a_1))\end{aligned}$
 \postw
 
 The variable $f$ is bound within the scope of $x$; therefore, $f$ depends on

--- a/src/Doc/Sledgehammer/document/root.tex	Wed Apr 10 11:32:48 2024 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Wed Apr 10 13:23:00 2024 +0200
@@ -36,7 +36,7 @@
 \def\rparr{\mathclose{\mid\mkern-4mu)}}
 
 \def\unk{{?}}
-\def\undef{(\lambda x.\; \unk)}
+\def\undefined{(\lambda x.\; \unk)}
 %\def\unr{\textit{others}}
 \def\unr{\ldots}
 \def\Abs#1{\hbox{\rm{\guillemetleft}}{\,#1\,}\hbox{\rm{\guillemetright}}}