src/HOL/Random_Pred.thy
changeset 51143 0a2371e7ced3
parent 51126 df86080de4cb
child 58889 5b7a9633cfa8
--- 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 \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a::random) Predicate.pred"
+fun iter' :: "'a itself \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> ('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 \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a::random) Predicate.pred"
+definition iter :: "natural \<Rightarrow> natural \<Rightarrow> Random.seed \<Rightarrow> ('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 \<Rightarrow> 'a) => code_numeral \<Rightarrow> code_numeral \<Rightarrow> 'a random_pred"
+definition iterate_upto :: "(natural \<Rightarrow> 'a) => natural \<Rightarrow> natural \<Rightarrow> 'a random_pred"
 where
   "iterate_upto f n m = Pair (Predicate.iterate_upto f n m)"