src/HOL/Random.thy
changeset 39302 d7728f65b353
parent 39198 f967a16dfcdd
child 42163 392fd6c4669c
     1.1 --- a/src/HOL/Random.thy	Mon Sep 13 08:43:48 2010 +0200
     1.2 +++ b/src/HOL/Random.thy	Mon Sep 13 11:13:15 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: ext_iff)
     1.8 +  by (induct xs) (auto simp add: fun_eq_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 -      ext_iff pick_same [symmetric])
    1.17 +      fun_eq_iff pick_same [symmetric])
    1.18  qed
    1.19  
    1.20