| changeset 995 | 95c148a7b9c4 |
| parent 974 | 68d58134fad6 |
| child 1169 | 5873833cf37f |
--- a/src/HOL/List.ML Fri Mar 31 15:08:49 1995 +0200 +++ b/src/HOL/List.ML Sun Apr 02 10:43:59 1995 +0200 @@ -134,7 +134,8 @@ (** Additional mapping lemmas **) -goal List.thy "map (%x.x) xs = xs"; +goal List.thy "map (%x.x) = (%xs.xs)"; +by (rtac ext 1); by (list.induct_tac "xs" 1); by (ALLGOALS (asm_simp_tac list_ss)); qed "map_ident";