equal
deleted
inserted
replaced
71 "mirror(C ts) = C(rev(map mirror ts))" |
71 "mirror(C ts) = C(rev(map mirror ts))" |
72 (hints recdef_simp: termi_lem) |
72 (hints recdef_simp: termi_lem) |
73 |
73 |
74 lemma "mirror(mirror t) = t" |
74 lemma "mirror(mirror t) = t" |
75 apply(induct_tac t rule: mirror.induct) |
75 apply(induct_tac t rule: mirror.induct) |
76 apply(simp add:rev_map sym[OF map_compose] cong:map_cong) |
76 apply(simp add: rev_map sym[OF map_compose] cong: map_cong) |
77 done |
77 done |
78 |
78 |
79 text{* |
79 text{* |
80 \begin{exercise} |
80 \begin{exercise} |
81 Define a function for merging two ordered lists (of natural numbers) and |
81 Define a function for merging two ordered lists (of natural numbers) and |