equal
deleted
inserted
replaced
5 \isa{flatten} from trees to lists. The straightforward version of |
5 \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. |
6 \isa{flatten} is based on \isa{\at} and is thus, like \isa{rev}, quadratic. |
7 A linear time version of \isa{flatten} again reqires an extra |
7 A linear time version of \isa{flatten} again reqires an extra |
8 argument, the accumulator:% |
8 argument, the accumulator:% |
9 \end{isamarkuptext}% |
9 \end{isamarkuptext}% |
10 \isacommand{consts}~flatten2~::~{"}'a~tree~=>~'a~list~=>~'a~list{"}% |
10 \isacommand{consts}\ flatten2\ ::\ {"}'a\ tree\ =>\ 'a\ list\ =>\ 'a\ list{"}% |
11 \begin{isamarkuptext}% |
11 \begin{isamarkuptext}% |
12 \noindent Define \isa{flatten2} and prove% |
12 \noindent Define \isa{flatten2} and prove% |
13 \end{isamarkuptext}% |
13 \end{isamarkuptext}% |
14 \isacommand{lemma}~{"}flatten2~t~[]~=~flatten~t{"}\end{isabelle}% |
14 \isacommand{lemma}\ {"}flatten2\ t\ []\ =\ flatten\ t{"}\end{isabelle}% |
15 %%% Local Variables: |
15 %%% Local Variables: |
16 %%% mode: latex |
16 %%% mode: latex |
17 %%% TeX-master: "root" |
17 %%% TeX-master: "root" |
18 %%% End: |
18 %%% End: |