src/HOL/Random.thy
changeset 46311 56fae81902ce
parent 44921 58eef4843641
child 51143 0a2371e7ced3
     1.1 --- a/src/HOL/Random.thy	Mon Jan 23 11:59:00 2012 +0100
     1.2 +++ b/src/HOL/Random.thy	Mon Jan 23 14:00:52 2012 +0100
     1.3 @@ -114,7 +114,7 @@
     1.4    "select_weight ((0, x) # xs) = select_weight xs"
     1.5    by (simp add: select_weight_def)
     1.6  
     1.7 -lemma select_weigth_drop_zero:
     1.8 +lemma select_weight_drop_zero:
     1.9    "select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs"
    1.10  proof -
    1.11    have "listsum (map fst [(k, _)\<leftarrow>xs . 0 < k]) = listsum (map fst xs)"
    1.12 @@ -122,7 +122,7 @@
    1.13    then show ?thesis by (simp only: select_weight_def pick_drop_zero)
    1.14  qed
    1.15  
    1.16 -lemma select_weigth_select:
    1.17 +lemma select_weight_select:
    1.18    assumes "xs \<noteq> []"
    1.19    shows "select_weight (map (Pair 1) xs) = select xs"
    1.20  proof -