src/HOL/Random.thy
changeset 39198 f967a16dfcdd
parent 37751 89e16802b6cc
child 39302 d7728f65b353
     1.1 --- a/src/HOL/Random.thy	Mon Sep 06 22:58:06 2010 +0200
     1.2 +++ b/src/HOL/Random.thy	Tue Sep 07 10:05:19 2010 +0200
     1.3 @@ -85,7 +85,7 @@
     1.4  
     1.5  lemma pick_drop_zero:
     1.6    "pick (filter (\<lambda>(k, _). k > 0) xs) = pick xs"
     1.7 -  by (induct xs) (auto simp add: expand_fun_eq)
     1.8 +  by (induct xs) (auto simp add: ext_iff)
     1.9  
    1.10  lemma pick_same:
    1.11    "l < length xs \<Longrightarrow> Random.pick (map (Pair 1) xs) (Code_Numeral.of_nat l) = nth xs l"
    1.12 @@ -132,7 +132,7 @@
    1.13      by (induct xs) simp_all
    1.14    ultimately show ?thesis
    1.15      by (auto simp add: select_weight_def select_def scomp_def split_def
    1.16 -      expand_fun_eq pick_same [symmetric])
    1.17 +      ext_iff pick_same [symmetric])
    1.18  qed
    1.19  
    1.20