src/HOL/Probability/SPMF.thy
changeset 63540 f8652d0534fa
parent 63343 fb5d8a50c641
child 63566 e5abbdee461a
     1.1 --- a/src/HOL/Probability/SPMF.thy	Fri Jul 22 08:02:37 2016 +0200
     1.2 +++ b/src/HOL/Probability/SPMF.thy	Fri Jul 22 11:00:43 2016 +0200
     1.3 @@ -2520,8 +2520,8 @@
     1.4      ultimately have "(weight_spmf p * weight_spmf q) * (weight_spmf p * weight_spmf q) = 1" by simp
     1.5      hence *: "weight_spmf p * weight_spmf q = 1"
     1.6        by(metis antisym_conv less_le mult_less_cancel_left1 weight_pair_spmf weight_spmf_le_1 weight_spmf_nonneg)
     1.7 -    hence "weight_spmf p = 1" by(metis antisym_conv mult_left_le weight_spmf_le_1 weight_spmf_nonneg)
     1.8 -    moreover with * have "weight_spmf q = 1" by simp
     1.9 +    hence **: "weight_spmf p = 1" by(metis antisym_conv mult_left_le weight_spmf_le_1 weight_spmf_nonneg)
    1.10 +    moreover from * ** have "weight_spmf q = 1" by simp
    1.11      moreover note calculation }
    1.12    note full = this
    1.13