src/HOL/Probability/Levy.thy

   have tight: "tight M"
     by (auto simp: tight_def intro: assms tight_aux)
   show ?thesis
   proof (rule tight_subseq_weak_converge [OF real_distr_M real_distr_M' tight])
     fix s \<nu>
-    assume s: "subseq s"
+    assume s: "strict_mono (s :: nat \<Rightarrow> nat)"
     assume nu: "weak_conv_m (M \<circ> s) \<nu>"
     assume *: "real_distribution \<nu>"
     have 2: "\<And>n. real_distribution ((M \<circ> s) n)" unfolding comp_def by (rule assms)
     have 3: "\<And>t. (\<lambda>n. char ((M \<circ> s) n) t) \<longlonglongrightarrow> char \<nu> t" by (intro levy_continuity1 [OF 2 * nu])
     have 4: "\<And>t. (\<lambda>n. char ((M \<circ> s) n) t) = ((\<lambda>n. char (M n) t) \<circ> s)" by (rule ext, simp)