--- a/src/HOL/Probability/Distributions.thy Sun Apr 24 21:31:14 2016 +0200
+++ b/src/HOL/Probability/Distributions.thy Mon Apr 25 16:09:26 2016 +0200
@@ -1216,7 +1216,7 @@
shows "(\<lambda>x. \<integral>\<^sup>+y. ennreal (normal_density 0 \<sigma> (x - y) * normal_density 0 \<tau> y) \<partial>lborel) =
normal_density 0 (sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2))" (is "?LHS = ?RHS")
proof -
- def \<sigma>' \<equiv> "\<sigma>\<^sup>2" and \<tau>' \<equiv> "\<tau>\<^sup>2"
+ define \<sigma>' \<tau>' where "\<sigma>' = \<sigma>\<^sup>2" and "\<tau>' = \<tau>\<^sup>2"
then have [simp, arith]: "0 < \<sigma>'" "0 < \<tau>'"
by simp_all
let ?\<sigma> = "sqrt ((\<sigma>' * \<tau>') / (\<sigma>' + \<tau>'))"