equal
deleted
inserted
replaced
1 \begin{isabelle}% |
1 % |
|
2 \begin{isabellebody}% |
2 % |
3 % |
3 \begin{isamarkuptext}% |
4 \begin{isamarkuptext}% |
4 \noindent In Exercise~\ref{ex:Tree} we defined a function |
5 \noindent In Exercise~\ref{ex:Tree} we defined a function |
5 \isa{flatten} from trees to lists. The straightforward version of |
6 \isa{flatten} from trees to lists. The straightforward version of |
6 \isa{flatten} is based on \isa{\at} and is thus, like \isa{rev}, quadratic. |
7 \isa{flatten} is based on \isa{\at} and is thus, like \isa{rev}, quadratic. |
9 \end{isamarkuptext}% |
10 \end{isamarkuptext}% |
10 \isacommand{consts}\ flatten\isadigit{2}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list{\isachardoublequote}% |
11 \isacommand{consts}\ flatten\isadigit{2}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list{\isachardoublequote}% |
11 \begin{isamarkuptext}% |
12 \begin{isamarkuptext}% |
12 \noindent Define \isa{flatten2} and prove% |
13 \noindent Define \isa{flatten2} and prove% |
13 \end{isamarkuptext}% |
14 \end{isamarkuptext}% |
14 \isacommand{lemma}\ {\isachardoublequote}flatten\isadigit{2}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\end{isabelle}% |
15 \isacommand{lemma}\ {\isachardoublequote}flatten\isadigit{2}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\end{isabellebody}% |
15 %%% Local Variables: |
16 %%% Local Variables: |
16 %%% mode: latex |
17 %%% mode: latex |
17 %%% TeX-master: "root" |
18 %%% TeX-master: "root" |
18 %%% End: |
19 %%% End: |