# HG changeset patch
# User haftmann
# Date 1243351773 -7200
# Node ID 900ebbc35e30f3ef1ed6670853971a930735505f
# Parent  4d273d043d59992ebe83de7b0e356cbe503ac842
dropped superfluos prefixes

diff -r 4d273d043d59 -r 900ebbc35e30 src/HOL/Random.thy
--- a/src/HOL/Random.thy	Tue May 26 17:29:32 2009 +0200
+++ b/src/HOL/Random.thy	Tue May 26 17:29:33 2009 +0200
@@ -119,7 +119,7 @@
 qed
 
 lemma select_weigth_drop_zero:
-  "Random.select_weight (filter (\<lambda>(k, _). k > 0) xs) = Random.select_weight xs"
+  "select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs"
 proof -
   have "listsum (map fst [(k, _)\<leftarrow>xs . 0 < k]) = listsum (map fst xs)"
     by (induct xs) auto
@@ -128,9 +128,9 @@
 
 lemma select_weigth_select:
   assumes "xs \<noteq> []"
-  shows "Random.select_weight (map (Pair 1) xs) = Random.select xs"
+  shows "select_weight (map (Pair 1) xs) = select xs"
 proof -
-  have less: "\<And>s. fst (Random.range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)"
+  have less: "\<And>s. fst (range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)"
     using assms by (intro range) simp
   moreover have "listsum (map fst (map (Pair 1) xs)) = Code_Numeral.of_nat (length xs)"
     by (induct xs) simp_all