diff -r ac9e909fe55d -r 0a2371e7ced3 src/HOL/Random_Pred.thy --- a/src/HOL/Random_Pred.thy Fri Feb 15 08:31:30 2013 +0100 +++ b/src/HOL/Random_Pred.thy Fri Feb 15 08:31:31 2013 +0100 @@ -7,13 +7,13 @@ imports Quickcheck_Random begin -fun iter' :: "'a itself \ code_numeral \ code_numeral \ Random.seed \ ('a::random) Predicate.pred" +fun iter' :: "'a itself \ natural \ natural \ Random.seed \ ('a::random) Predicate.pred" where "iter' T nrandom sz seed = (if nrandom = 0 then bot_class.bot else let ((x, _), seed') = Quickcheck_Random.random sz seed in Predicate.Seq (%u. Predicate.Insert x (iter' T (nrandom - 1) sz seed')))" -definition iter :: "code_numeral \ code_numeral \ Random.seed \ ('a::random) Predicate.pred" +definition iter :: "natural \ natural \ Random.seed \ ('a::random) Predicate.pred" where "iter nrandom sz seed = iter' (TYPE('a)) nrandom sz seed" @@ -48,7 +48,7 @@ where "if_randompred b = (if b then single () else empty)" -definition iterate_upto :: "(code_numeral \ 'a) => code_numeral \ code_numeral \ 'a random_pred" +definition iterate_upto :: "(natural \ 'a) => natural \ natural \ 'a random_pred" where "iterate_upto f n m = Pair (Predicate.iterate_upto f n m)"