changeset 45129 | 1fce03e3e8ad |
parent 44263 | 971d1be5d5ce |
child 45990 | b7b905b23b2a |
--- a/src/HOL/Quotient_Examples/DList.thy Wed Oct 12 16:21:07 2011 +0200 +++ b/src/HOL/Quotient_Examples/DList.thy Wed Oct 12 20:16:48 2011 +0200 @@ -45,7 +45,7 @@ assumes "remdups xa = remdups ya" shows "remdups (map f xa) = remdups (map f ya)" using assms - by (induct xa ya arbitrary: fx fy rule: list_induct2') + by (induct xa ya rule: list_induct2') (metis (full_types) remdups_nil_noteq_cons(2) remdups_map_remdups)+ lemma remdups_eq_member_eq: