src/HOL/List.thy
changeset 41505 6d19301074cf
parent 41463 edbf0a86fb1c
child 41697 19890332febc
     1.1 --- a/src/HOL/List.thy	Mon Jan 10 22:03:24 2011 +0100
     1.2 +++ b/src/HOL/List.thy	Tue Jan 11 14:12:37 2011 +0100
     1.3 @@ -880,7 +880,7 @@
     1.4    "length xs = length ys \<Longrightarrow> map snd (zip xs ys) = ys"
     1.5  by (induct rule:list_induct2, simp_all)
     1.6  
     1.7 -type_lifting map: map
     1.8 +enriched_type map: map
     1.9    by (simp_all add: fun_eq_iff id_def)
    1.10  
    1.11