1.1 --- a/src/HOL/Random.thy	Sun Jun 14 09:13:59 2009 +0200
     1.2 +++ b/src/HOL/Random.thy	Sun Jun 14 17:20:19 2009 +0200
     1.3 @@ -143,28 +143,6 @@
     1.4        expand_fun_eq pick_same [symmetric])
     1.5  qed
     1.6  
     1.7 -definition select_default :: "code_numeral \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
     1.8 -  [code del]: "select_default k x y = range k
     1.9 -     o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))"
    1.10 -
    1.11 -lemma select_default_zero:
    1.12 -  "fst (select_default 0 x y s) = y"
    1.13 -  by (simp add: scomp_apply split_beta select_default_def)
    1.14 -
    1.15 -lemma select_default_code [code]:
    1.16 -  "select_default k x y = (if k = 0
    1.17 -    then range 1 o\<rightarrow> (\<lambda>_. Pair y)
    1.18 -    else range k o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y)))"
    1.19 -proof
    1.20 -  fix s
    1.21 -  have "snd (range (Code_Numeral.of_nat 0) s) = snd (range (Code_Numeral.of_nat 1) s)"
    1.22 -    by (simp add: range_def scomp_Pair scomp_apply split_beta)
    1.23 -  then show "select_default k x y s = (if k = 0
    1.24 -    then range 1 o\<rightarrow> (\<lambda>_. Pair y)
    1.25 -    else range k o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))) s"
    1.26 -    by (cases "k = 0") (simp_all add: select_default_def scomp_apply split_beta)
    1.27 -qed
    1.28 -
    1.29  
    1.30  subsection {* @{text ML} interface *}
    1.31