equal
deleted
inserted
replaced
12 "flatten2 (Node l x r) xs = flatten2 l (x#(flatten2 r xs))" |
12 "flatten2 (Node l x r) xs = flatten2 l (x#(flatten2 r xs))" |
13 (*>*) |
13 (*>*) |
14 |
14 |
15 text\<open>\noindent and prove\<close> |
15 text\<open>\noindent and prove\<close> |
16 (*<*) |
16 (*<*) |
17 lemma [simp]: "!xs. flatten2 t xs = flatten t @ xs" |
17 lemma [simp]: "\<forall>xs. flatten2 t xs = flatten t @ xs" |
18 apply(induct_tac t) |
18 apply(induct_tac t) |
19 by(auto) |
19 by(auto) |
20 (*>*) |
20 (*>*) |
21 lemma "flatten2 t [] = flatten t" |
21 lemma "flatten2 t [] = flatten t" |
22 (*<*) |
22 (*<*) |