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