equal
deleted
inserted
replaced
9 \isa{flatten} is based on \isa{{\isacharat}} and is thus, like \isa{rev}, |
9 \isa{flatten} is based on \isa{{\isacharat}} and is thus, like \isa{rev}, |
10 quadratic. A linear time version of \isa{flatten} again reqires an extra |
10 quadratic. A linear time version of \isa{flatten} again reqires an extra |
11 argument, the accumulator:% |
11 argument, the accumulator:% |
12 \end{isamarkuptext}% |
12 \end{isamarkuptext}% |
13 \isamarkuptrue% |
13 \isamarkuptrue% |
14 \isacommand{consts}\ flatten{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isamarkupfalse% |
14 \isacommand{consts}\ flatten{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline |
|
15 \isamarkupfalse% |
15 \isamarkupfalse% |
16 \isamarkupfalse% |
16 % |
17 % |
17 \begin{isamarkuptext}% |
18 \begin{isamarkuptext}% |
18 \noindent Define \isa{flatten{\isadigit{2}}} and prove% |
19 \noindent Define \isa{flatten{\isadigit{2}}} and prove% |
19 \end{isamarkuptext}% |
20 \end{isamarkuptext}% |
20 \isamarkuptrue% |
21 \isamarkuptrue% |
21 \isamarkupfalse% |
22 \isamarkupfalse% |
22 \isamarkupfalse% |
23 \isamarkupfalse% |
23 \isanewline |
|
24 \isamarkupfalse% |
24 \isamarkupfalse% |
25 \isacommand{lemma}\ {\isachardoublequote}flatten{\isadigit{2}}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\isamarkupfalse% |
25 \isacommand{lemma}\ {\isachardoublequote}flatten{\isadigit{2}}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\isanewline |
26 \isamarkupfalse% |
26 \isamarkupfalse% |
27 \isanewline |
27 \isamarkupfalse% |
28 \isamarkupfalse% |
28 \isamarkupfalse% |
29 \end{isabellebody}% |
29 \end{isabellebody}% |
30 %%% Local Variables: |
30 %%% Local Variables: |
31 %%% mode: latex |
31 %%% mode: latex |
32 %%% TeX-master: "root" |
32 %%% TeX-master: "root" |