src/HOL/Quickcheck.thy
changeset 50046 0051dc4f301f
parent 49972 f11f8905d9fd
     1.1 --- a/src/HOL/Quickcheck.thy	Sun Nov 11 19:24:01 2012 +0100
     1.2 +++ b/src/HOL/Quickcheck.thy	Sun Nov 11 19:56:02 2012 +0100
     1.3 @@ -157,11 +157,11 @@
     1.4        (i, random j \<circ>\<rightarrow> (%x. random_aux_set (i - 1) j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
     1.5  proof (induct i rule: code_numeral.induct)
     1.6    case zero
     1.7 -  show ?case by (subst select_weight_drop_zero[symmetric])
     1.8 -    (simp add: filter.simps random_aux_set.simps[simplified])
     1.9 +  show ?case by (subst select_weight_drop_zero [symmetric])
    1.10 +    (simp add: random_aux_set.simps [simplified])
    1.11  next
    1.12    case (Suc i)
    1.13 -  show ?case by (simp only: random_aux_set.simps(2)[of "i"] Suc_code_numeral_minus_one)
    1.14 +  show ?case by (simp only: random_aux_set.simps(2) [of "i"] Suc_code_numeral_minus_one)
    1.15  qed
    1.16  
    1.17  definition "random_set i = random_aux_set i i"