# HG changeset patch # User wenzelm # Date 1712748180 -7200 # Node ID 1a9f0159de5b3cc6801b4282b66166bff005cd8f # Parent 646cd337bb0836adff89d429c110d5c39aedd9f1# Parent 36389d25d33e05bfc7c4071824668758c0145d08 merged diff -r 646cd337bb08 -r 1a9f0159de5b src/Doc/Nitpick/document/root.tex --- 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 diff -r 646cd337bb08 -r 1a9f0159de5b src/Doc/Sledgehammer/document/root.tex --- 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}}}