--- a/src/HOL/Probability/Characteristic_Functions.thy Sun Apr 24 21:31:14 2016 +0200
+++ b/src/HOL/Probability/Characteristic_Functions.thy Mon Apr 25 16:09:26 2016 +0200
@@ -308,7 +308,7 @@
have integ_iexp: "integrable M (\<lambda>x. iexp (t * x))"
by (intro integrable_const_bound) auto
- def c \<equiv> "\<lambda>k x. (ii * t)^k / fact k * complex_of_real (x^k)"
+ define c where [abs_def]: "c k x = (ii * t)^k / fact k * complex_of_real (x^k)" for k x
have integ_c: "\<And>k. k \<le> n \<Longrightarrow> integrable M (\<lambda>x. c k x)"
unfolding c_def by (intro integrable_mult_right integrable_of_real integrable_moments)
@@ -343,7 +343,7 @@
have integ_iexp: "integrable M (\<lambda>x. iexp (t * x))"
by (intro integrable_const_bound) auto
- def c \<equiv> "\<lambda>k x. (ii * t)^k / fact k * complex_of_real (x^k)"
+ define c where [abs_def]: "c k x = (ii * t)^k / fact k * complex_of_real (x^k)" for k x
have integ_c: "\<And>k. k \<le> n \<Longrightarrow> integrable M (\<lambda>x. c k x)"
unfolding c_def by (intro integrable_mult_right integrable_of_real integrable_moments)