changeset 41372 | 551eb49a6e91 |
parent 41311 | de0c906dfe60 |
child 41505 | 6d19301074cf |
--- a/src/HOL/Predicate.thy Tue Dec 21 16:14:46 2010 +0100 +++ b/src/HOL/Predicate.thy Tue Dec 21 17:52:23 2010 +0100 @@ -795,8 +795,8 @@ "eval (map f P) = image f (eval P)" by (auto simp add: map_def) -type_lifting map - by (auto intro!: pred_eqI simp add: image_image) +type_lifting map: map + by (auto intro!: pred_eqI simp add: fun_eq_iff image_compose) subsubsection {* Implementation *}