tuned op's
authornipkow
Thu Dec 21 21:38:23 2017 +0100 (19 months ago)
changeset 6724173635a5bfa5c
parent 67240 2c9694a8c000
child 67242 a6d8458b48c0
tuned op's
src/HOL/Analysis/Embed_Measure.thy
     1.1 --- a/src/HOL/Analysis/Embed_Measure.thy	Thu Dec 21 21:01:47 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Embed_Measure.thy	Thu Dec 21 21:38:23 2017 +0100
     1.3 @@ -189,7 +189,7 @@
     1.4    by(rule embed_measure_count_space')(erule subset_inj_on, simp)
     1.5  
     1.6  lemma sets_embed_measure_alt:
     1.7 -    "inj f \<Longrightarrow> sets (embed_measure M f) = (op`f) ` sets M"
     1.8 +    "inj f \<Longrightarrow> sets (embed_measure M f) = (op` f) ` sets M"
     1.9    by (auto simp: sets_embed_measure)
    1.10  
    1.11  lemma emeasure_embed_measure_image':