summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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