src/HOL/Probability/Helly_Selection.thy

     ultimately have "\<exists>l s'. subseq s' \<and> ((\<lambda>k. f (s k) (r n)) \<circ> s') \<longlonglongrightarrow> l"
       using compact_Icc compact_imp_seq_compact seq_compactE by metis
     thus "\<exists>s'. subseq s' \<and> (\<exists>l. (\<lambda>k. f (s (s' k)) (r n)) \<longlonglongrightarrow> l)"
       by (auto simp: comp_def)
   qed
-  def d \<equiv> "nat.diagseq"
+  define d where "d = nat.diagseq"
   have subseq: "subseq d"
     unfolding d_def using nat.subseq_diagseq by auto
   have rat_cnv: "?P n d" for n
   proof -
     have Pn_seqseq: "?P n (nat.seqseq (Suc n))"

   have r_unbdd: "\<exists>n. x < r n" for x
     using dense_r[OF less_add_one, of x] by auto
   then have nonempty: "{lim (?f n) |n. x < r n} \<noteq> {}" for x
     by auto
 
-  def F \<equiv> "\<lambda>x. Inf {lim (?f n) |n. x < r n}"
+  define F where "F x = Inf {lim (?f n) |n. x < r n}" for x
   have F_eq: "ereal (F x) = (INF n:{n. x < r n}. ereal (lim (?f n)))" for x
     unfolding F_def by (subst ereal_Inf'[OF bdd_below nonempty]) (simp add: setcompr_eq_image)
   have mono_F: "mono F"
     using nonempty by (auto intro!: cInf_superset_mono simp: F_def bdd_below mono_def)
   moreover have "\<And>x. continuous (at_right x) F"

 (* Can strengthen to equivalence. *)
 theorem tight_imp_convergent_subsubsequence:
   assumes \<mu>: "tight \<mu>" "subseq s"
   shows "\<exists>r M. subseq r \<and> real_distribution M \<and> weak_conv_m (\<mu> \<circ> s \<circ> r) M"
 proof -
-  def f \<equiv> "\<lambda>k. cdf (\<mu> (s k))"
+  define f where "f k = cdf (\<mu> (s k))" for k
   interpret \<mu>: real_distribution "\<mu> k" for k
     using \<mu> unfolding tight_def by auto
 
   have rcont: "\<And>x. continuous (at_right x) (f k)"
     and mono: "mono (f k)"

   fixes \<mu> :: "nat \<Rightarrow> real measure" and M :: "real measure"
   assumes "\<And>n. real_distribution (\<mu> n)" "real_distribution M" and tight: "tight \<mu>" and
     subseq: "\<And>s \<nu>. subseq s \<Longrightarrow> real_distribution \<nu> \<Longrightarrow> weak_conv_m (\<mu> \<circ> s) \<nu> \<Longrightarrow> weak_conv_m (\<mu> \<circ> s) M"
   shows "weak_conv_m \<mu> M"
 proof (rule ccontr)
-  def f \<equiv> "\<lambda>n. cdf (\<mu> n)" and F \<equiv> "cdf M"
+  define f where "f n = cdf (\<mu> n)" for n
+  define F where "F = cdf M"
 
   assume "\<not> weak_conv_m \<mu> M"
   then obtain x where x: "isCont F x" "\<not> (\<lambda>n. f n x) \<longlonglongrightarrow> F x"
     by (auto simp: weak_conv_m_def weak_conv_def f_def F_def)
   then obtain \<epsilon> where "\<epsilon> > 0" and "infinite {n. \<not> dist (f n x) (F x) < \<epsilon>}"