src/HOL/Probability/Independent_Family.thy

     let ?G = "\<lambda>S i. if i \<in> S then ?F i else F i"
     assume "finite J" "J \<subseteq> K"
     then have "indep_sets (?G J) K"
     proof induct
       case (insert j J)
-      moreover def G \<equiv> "?G J"
+      moreover define G where "G = ?G J"
       ultimately have G: "indep_sets G K" "\<And>i. i \<in> K \<Longrightarrow> G i \<subseteq> events" and "j \<in> K"
         by (auto simp: indep_sets_def)
       let ?D = "{E\<in>events. indep_sets (G(j := {E})) K }"
       { fix X assume X: "X \<in> events"
         assume indep: "\<And>J A. J \<noteq> {} \<Longrightarrow> J \<subseteq> K \<Longrightarrow> finite J \<Longrightarrow> j \<notin> J \<Longrightarrow> (\<forall>i\<in>J. A i \<in> G i)

           with L(2,3)[OF \<open>j \<in> K\<close>] L(2,3)[OF \<open>k \<in> K\<close>]
           show False using \<open>l \<in> L k\<close> \<open>l \<in> L j\<close> by auto
         qed }
       note L_inj = this
 
-      def k \<equiv> "\<lambda>l. (SOME k. k \<in> K \<and> l \<in> L k)"
+      define k where "k l = (SOME k. k \<in> K \<and> l \<in> L k)" for l
       { fix x j l assume *: "j \<in> K" "l \<in> L j"
         have "k l = j" unfolding k_def
         proof (rule some_equality)
           fix k assume "k \<in> K \<and> l \<in> L k"
           with * L_inj show "k = j" by auto

 lemma (in prob_space) indep_vars_nn_integral:
   assumes I: "finite I" "indep_vars (\<lambda>_. borel) X I" "\<And>i \<omega>. i \<in> I \<Longrightarrow> 0 \<le> X i \<omega>"
   shows "(\<integral>\<^sup>+\<omega>. (\<Prod>i\<in>I. X i \<omega>) \<partial>M) = (\<Prod>i\<in>I. \<integral>\<^sup>+\<omega>. X i \<omega> \<partial>M)"
 proof cases
   assume "I \<noteq> {}"
-  def Y \<equiv> "\<lambda>i \<omega>. if i \<in> I then X i \<omega> else 0"
+  define Y where [abs_def]: "Y i \<omega> = (if i \<in> I then X i \<omega> else 0)" for i \<omega>
   { fix i have "i \<in> I \<Longrightarrow> random_variable borel (X i)"
     using I(2) by (cases "i\<in>I") (auto simp: indep_vars_def) }
   note rv_X = this
 
   { fix i have "random_variable borel (Y i)"

   assumes I: "finite I" "indep_vars (\<lambda>_. borel) X I" "\<And>i. i \<in> I \<Longrightarrow> integrable M (X i)"
   shows indep_vars_lebesgue_integral: "(\<integral>\<omega>. (\<Prod>i\<in>I. X i \<omega>) \<partial>M) = (\<Prod>i\<in>I. \<integral>\<omega>. X i \<omega> \<partial>M)" (is ?eq)
     and indep_vars_integrable: "integrable M (\<lambda>\<omega>. (\<Prod>i\<in>I. X i \<omega>))" (is ?int)
 proof (induct rule: case_split)
   assume "I \<noteq> {}"
-  def Y \<equiv> "\<lambda>i \<omega>. if i \<in> I then X i \<omega> else 0"
+  define Y where [abs_def]: "Y i \<omega> = (if i \<in> I then X i \<omega> else 0)" for i \<omega>
   { fix i have "i \<in> I \<Longrightarrow> random_variable borel (X i)"
     using I(2) by (cases "i\<in>I") (auto simp: indep_vars_def) }
   note rv_X = this[measurable]
 
   { fix i have "random_variable borel (Y i)"