src/HOL/Random.thy

       (\<lambda>l. next \<circ>\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1
     \<circ>\<rightarrow> (\<lambda>v. Pair (v mod k))"
 
 lemma range:
   "k > 0 \<Longrightarrow> fst (range k s) < k"
-  by (simp add: range_def scomp_apply split_def del: log.simps iterate.simps)
+  by (simp add: range_def split_def del: log.simps iterate.simps)
 
 definition select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
   "select xs = range (Code_Numeral.of_nat (length xs))
     \<circ>\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Numeral.nat_of k)))"
      

   with range have
     "fst (range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)" by best
   then have
     "Code_Numeral.nat_of (fst (range (Code_Numeral.of_nat (length xs)) s)) < length xs" by simp
   then show ?thesis
-    by (simp add: scomp_apply split_beta select_def)
+    by (simp add: split_beta select_def)
 qed
 
 primrec pick :: "(code_numeral \<times> 'a) list \<Rightarrow> code_numeral \<Rightarrow> 'a" where
   "pick (x # xs) i = (if i < fst x then snd x else pick xs (i - fst x))"
 

 
 no_notation fcomp (infixl "\<circ>>" 60)
 no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
 end
-