changeset 55467 | a5c9002bc54d |
parent 55416 | dd7992d4a61a |
child 56154 | f0a927235162 |
--- a/src/HOL/Predicate.thy Fri Feb 14 07:53:46 2014 +0100 +++ b/src/HOL/Predicate.thy Fri Feb 14 07:53:46 2014 +0100 @@ -396,7 +396,7 @@ "eval (map f P) = (\<Squnion>x\<in>{x. eval P x}. (\<lambda>y. f x = y))" by (auto simp add: map_def comp_def) -enriched_type map: map +functor map: map by (rule ext, rule pred_eqI, auto)+