Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Probability/Borel.thy
changeset 39083 e46acc0ea1fe
parent 38705 aaee86c0e237
child 39087 96984bf6fa5b 
--- a/src/HOL/Probability/Borel.thy	Thu Aug 26 15:20:41 2010 +0200
+++ b/src/HOL/Probability/Borel.thy	Thu Aug 26 18:41:54 2010 +0200
@@ -81,7 +81,7 @@
   "(\<lambda>x. c) \<in> borel_measurable M"
   by (auto intro!: measurable_const)
 
-lemma (in sigma_algebra) borel_measurable_indicator:
+lemma (in sigma_algebra) borel_measurable_indicator[simp, intro!]:
   assumes A: "A \<in> sets M"
   shows "indicator A \<in> borel_measurable M"
   unfolding indicator_def_raw using A
isabelle