src/HOL/Metis_Examples/Abstraction.thy
changeset 55465 0d31c0546286
parent 46364 abab10d1f4a3
child 55932 68c5104d2204
--- a/src/HOL/Metis_Examples/Abstraction.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/Metis_Examples/Abstraction.thy	Fri Feb 14 07:53:45 2014 +0100
@@ -138,14 +138,14 @@
 
 lemma "map (\<lambda>x. (f x, g x)) xs = zip (map f xs) (map g xs)"
 apply (induct xs)
- apply (metis map.simps(1) zip_Nil)
+ apply (metis list.map(1) zip_Nil)
 by auto
 
 lemma
   "map (\<lambda>w. (w -> w, w \<times> w)) xs =
    zip (map (\<lambda>w. w -> w) xs) (map (\<lambda>w. w \<times> w) xs)"
 apply (induct xs)
- apply (metis map.simps(1) zip_Nil)
+ apply (metis list.map(1) zip_Nil)
 by auto
 
 lemma "(\<lambda>x. Suc (f x)) ` {x. even x} \<subseteq> A \<Longrightarrow> \<forall>x. even x --> Suc (f x) \<in> A"