equal
deleted
inserted
replaced
51 dropped, the above goal is solved, |
51 dropped, the above goal is solved, |
52 *} |
52 *} |
53 (*<*) |
53 (*<*) |
54 lemma "(case xs of [] \\<Rightarrow> zs | y#ys \\<Rightarrow> y#(ys@zs)) = xs@zs"; |
54 lemma "(case xs of [] \\<Rightarrow> zs | y#ys \\<Rightarrow> y#(ys@zs)) = xs@zs"; |
55 (*>*) |
55 (*>*) |
56 apply(simp split: list.split).; |
56 by(simp split: list.split); |
57 |
57 |
58 text{*\noindent% |
58 text{*\noindent% |
59 which \isacommand{apply}\isa{(simp)} alone will not do. |
59 which \isacommand{apply}\isa{(simp)} alone will not do. |
60 |
60 |
61 In general, every datatype $t$ comes with a theorem |
61 In general, every datatype $t$ comes with a theorem |