equal
deleted
inserted
replaced
7 \isa{flatten} from trees to lists. The straightforward version of |
7 \isa{flatten} from trees to lists. The straightforward version of |
8 \isa{flatten} is based on \isa{{\isacharat}} and is thus, like \isa{rev}, |
8 \isa{flatten} is based on \isa{{\isacharat}} and is thus, like \isa{rev}, |
9 quadratic. A linear time version of \isa{flatten} again reqires an extra |
9 quadratic. A linear time version of \isa{flatten} again reqires an extra |
10 argument, the accumulator:% |
10 argument, the accumulator:% |
11 \end{isamarkuptext}% |
11 \end{isamarkuptext}% |
12 \isacommand{consts}\ flatten\isadigit{2}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list{\isachardoublequote}% |
12 \isacommand{consts}\ flatten{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list{\isachardoublequote}% |
13 \begin{isamarkuptext}% |
13 \begin{isamarkuptext}% |
14 \noindent Define \isa{flatten\isadigit{2}} and prove% |
14 \noindent Define \isa{flatten{\isadigit{2}}} and prove% |
15 \end{isamarkuptext}% |
15 \end{isamarkuptext}% |
16 \isacommand{lemma}\ {\isachardoublequote}flatten\isadigit{2}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\end{isabellebody}% |
16 \isacommand{lemma}\ {\isachardoublequote}flatten{\isadigit{2}}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\end{isabellebody}% |
17 %%% Local Variables: |
17 %%% Local Variables: |
18 %%% mode: latex |
18 %%% mode: latex |
19 %%% TeX-master: "root" |
19 %%% TeX-master: "root" |
20 %%% End: |
20 %%% End: |