--- a/src/HOL/List.thy Thu Nov 28 15:44:34 2002 +0100
+++ b/src/HOL/List.thy Fri Nov 29 09:48:28 2002 +0100
@@ -431,10 +431,13 @@
lemma rev_map: "rev (map f xs) = map f (rev xs)"
by (induct xs) auto
+lemma map_eq_conv[simp]: "(map f xs = map g xs) = (!x : set xs. f x = g x)"
+by (induct xs) auto
+
lemma map_cong [recdef_cong]:
"xs = ys ==> (!!x. x : set ys ==> f x = g x) ==> map f xs = map g ys"
-- {* a congruence rule for @{text map} *}
-by (clarify, induct ys) auto
+by simp
lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])"
by (cases xs) auto