| changeset 14025 | d9b155757dc8 |
| parent 13122 | c63612ffb186 |
| child 14401 | 477380c74c1d |
--- a/src/HOL/List.ML Tue May 13 08:59:21 2003 +0200 +++ b/src/HOL/List.ML Wed May 14 10:22:09 2003 +0200 @@ -156,7 +156,7 @@ val map_compose = thm "map_compose"; val map_concat = thm "map_concat"; val map_cong = thm "map_cong"; -val map_eq_Cons = thm "map_eq_Cons"; +val map_eq_Cons_conv = thm "map_eq_Cons_conv"; val map_ext = thm "map_ext"; val map_ident = thm "map_ident"; val map_injective = thm "map_injective";