doc-src/Codegen/Thy/document/Inductive_Predicate.tex

 %
 \endisadelimquote
 %
 \isatagquote
 \isacommand{values}\isamarkupfalse%
-\ {\isacharbrackleft}mode{\isacharcolon}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool{\isacharbrackright}\ {\isadigit{2}}{\isadigit{0}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ {\isadigit{1}}{\isadigit{0}}\ n{\isacharbraceright}{\isachardoublequoteclose}\isanewline
-\isacommand{values}\isamarkupfalse%
-\ {\isacharbrackleft}mode{\isacharcolon}\ o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool{\isacharbrackright}\ {\isadigit{1}}{\isadigit{0}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ n\ {\isadigit{1}}{\isadigit{0}}{\isacharbraceright}{\isachardoublequoteclose}%
+\ {\isacharbrackleft}mode{\isacharcolon}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool{\isacharbrackright}\ {\isadigit{1}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ {\isadigit{1}}{\isadigit{0}}\ n{\isacharbraceright}{\isachardoublequoteclose}\ \isanewline
+\isacommand{values}\isamarkupfalse%
+\ {\isacharbrackleft}mode{\isacharcolon}\ o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool{\isacharbrackright}\ {\isadigit{1}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ n\ {\isadigit{1}}{\isadigit{0}}{\isacharbraceright}{\isachardoublequoteclose}%
 \endisatagquote
 {\isafoldquote}%
 %
 \isadelimquote
 %