diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Probability/SPMF.thy
--- a/src/HOL/Probability/SPMF.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Probability/SPMF.thy Fri Jul 22 11:00:43 2016 +0200
@@ -2520,8 +2520,8 @@
ultimately have "(weight_spmf p * weight_spmf q) * (weight_spmf p * weight_spmf q) = 1" by simp
hence *: "weight_spmf p * weight_spmf q = 1"
by(metis antisym_conv less_le mult_less_cancel_left1 weight_pair_spmf weight_spmf_le_1 weight_spmf_nonneg)
- hence "weight_spmf p = 1" by(metis antisym_conv mult_left_le weight_spmf_le_1 weight_spmf_nonneg)
- moreover with * have "weight_spmf q = 1" by simp
+ hence **: "weight_spmf p = 1" by(metis antisym_conv mult_left_le weight_spmf_le_1 weight_spmf_nonneg)
+ moreover from * ** have "weight_spmf q = 1" by simp
moreover note calculation }
note full = this