src/HOL/Random.thy
changeset 44921 58eef4843641
parent 42163 392fd6c4669c
child 46311 56fae81902ce
     1.1 --- a/src/HOL/Random.thy	Tue Sep 13 08:21:51 2011 -0700
     1.2 +++ b/src/HOL/Random.thy	Tue Sep 13 17:07:33 2011 -0700
     1.3 @@ -57,7 +57,7 @@
     1.4  
     1.5  lemma range:
     1.6    "k > 0 \<Longrightarrow> fst (range k s) < k"
     1.7 -  by (simp add: range_def scomp_apply split_def del: log.simps iterate.simps)
     1.8 +  by (simp add: range_def split_def del: log.simps iterate.simps)
     1.9  
    1.10  definition select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
    1.11    "select xs = range (Code_Numeral.of_nat (length xs))
    1.12 @@ -73,7 +73,7 @@
    1.13    then have
    1.14      "Code_Numeral.nat_of (fst (range (Code_Numeral.of_nat (length xs)) s)) < length xs" by simp
    1.15    then show ?thesis
    1.16 -    by (simp add: scomp_apply split_beta select_def)
    1.17 +    by (simp add: split_beta select_def)
    1.18  qed
    1.19  
    1.20  primrec pick :: "(code_numeral \<times> 'a) list \<Rightarrow> code_numeral \<Rightarrow> 'a" where
    1.21 @@ -188,4 +188,3 @@
    1.22  no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
    1.23  
    1.24  end
    1.25 -