equal
deleted
inserted
replaced
132 store_thm("nth_0",nth_0); |
132 store_thm("nth_0",nth_0); |
133 store_thm("nth_Suc",nth_Suc); |
133 store_thm("nth_Suc",nth_Suc); |
134 |
134 |
135 (** Additional mapping lemmas **) |
135 (** Additional mapping lemmas **) |
136 |
136 |
137 goal List.thy "map (%x.x) xs = xs"; |
137 goal List.thy "map (%x.x) = (%xs.xs)"; |
|
138 by (rtac ext 1); |
138 by (list.induct_tac "xs" 1); |
139 by (list.induct_tac "xs" 1); |
139 by (ALLGOALS (asm_simp_tac list_ss)); |
140 by (ALLGOALS (asm_simp_tac list_ss)); |
140 qed "map_ident"; |
141 qed "map_ident"; |
141 |
142 |
142 goal List.thy "map f (xs@ys) = map f xs @ map f ys"; |
143 goal List.thy "map f (xs@ys) = map f xs @ map f ys"; |