Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned op's
authornipkow
Thu, 21 Dec 2017 21:38:23 +0100
changeset 67241 73635a5bfa5c
parent 67240 2c9694a8c000
child 67242 a6d8458b48c0
tuned op's
src/HOL/Analysis/Embed_Measure.thy file | annotate | diff | comparison | revisions 
--- 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':
isabelle