src/HOL/Random.thy

--- a/src/HOL/Random.thy	Wed May 27 22:11:05 2009 +0200
+++ b/src/HOL/Random.thy	Wed May 27 22:11:06 2009 +0200
@@ -118,6 +118,10 @@
   then show ?thesis by (simp add: select_weight_def scomp_def split_def) 
 qed
 
+lemma select_weight_cons_zero:
+  "select_weight ((0, x) # xs) = select_weight xs"
+  by (simp add: select_weight_def)
+
 lemma select_weigth_drop_zero:
   "select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs"
 proof -