# HG changeset patch
# User nipkow
# Date 1513888703 -3600
# Node ID 73635a5bfa5c6e2f5e51f2248f6b70dfea54a5ed
# Parent  2c9694a8c000c5bc9a780955d446e15307504913
tuned op's

diff -r 2c9694a8c000 -r 73635a5bfa5c src/HOL/Analysis/Embed_Measure.thy
--- a/src/HOL/Analysis/Embed_Measure.thy	Thu Dec 21 21:01:47 2017 +0100
+++ b/src/HOL/Analysis/Embed_Measure.thy	Thu Dec 21 21:38:23 2017 +0100
@@ -189,7 +189,7 @@
   by(rule embed_measure_count_space')(erule subset_inj_on, simp)
 
 lemma sets_embed_measure_alt:
-    "inj f \<Longrightarrow> sets (embed_measure M f) = (op`f) ` sets M"
+    "inj f \<Longrightarrow> sets (embed_measure M f) = (op` f) ` sets M"
   by (auto simp: sets_embed_measure)
 
 lemma emeasure_embed_measure_image':