--- a/src/HOL/Random.thy Sun Mar 13 09:06:50 2016 +0100
+++ b/src/HOL/Random.thy Sun Mar 13 10:22:46 2016 +0100
@@ -1,4 +1,3 @@
-
(* Author: Florian Haftmann, TU Muenchen *)
section \<open>A HOL random engine\<close>
@@ -118,7 +117,7 @@
"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 simp add: less_natural_def, simp add: plus_natural_def)
+ by (induct xs) (auto simp add: less_natural_def natural_eq_iff)
then show ?thesis by (simp only: select_weight_def pick_drop_zero)
qed