src/HOL/Probability/Borel_Space.thy

   shows "(\<lambda>x. SUP i : A. f i x) \<in> borel_measurable M" (is "?sup \<in> borel_measurable M")
   unfolding borel_measurable_ereal_iff_ge
 proof
   fix a
   have "?sup -` {a<..} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. a < f i x})"
-    by (auto simp: less_SUP_iff SUPR_apply)
+    by (auto simp: less_SUP_iff SUP_apply)
   then show "?sup -` {a<..} \<inter> space M \<in> sets M"
     using assms by auto
 qed
 
 lemma (in sigma_algebra) borel_measurable_INF[simp, intro]:

   shows "(\<lambda>x. INF i : A. f i x) \<in> borel_measurable M" (is "?inf \<in> borel_measurable M")
   unfolding borel_measurable_ereal_iff_less
 proof
   fix a
   have "?inf -` {..<a} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. f i x < a})"
-    by (auto simp: INF_less_iff INFI_apply)
+    by (auto simp: INF_less_iff INF_apply)
   then show "?inf -` {..<a} \<inter> space M \<in> sets M"
     using assms by auto
 qed
 
 lemma (in sigma_algebra) borel_measurable_liminf[simp, intro]: