src/HOL/Quickcheck.thy
changeset 31985 a6e982b1ebba
parent 31641 feea4d3d743d
child 32373 c96330408d89
     1.1 --- a/src/HOL/Quickcheck.thy	Fri Jul 10 07:59:23 2009 +0200
     1.2 +++ b/src/HOL/Quickcheck.thy	Fri Jul 10 07:59:25 2009 +0200
     1.3 @@ -23,8 +23,8 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  "random i = Random.range i o\<rightarrow>
     1.8 -    (\<lambda>k. Pair (if (k div 2 = 0) then Code_Eval.valtermify True else Code_Eval.valtermify False))"
     1.9 +  "random i = Random.range 2 o\<rightarrow>
    1.10 +    (\<lambda>k. Pair (if k = 0 then Code_Eval.valtermify False else Code_Eval.valtermify True))"
    1.11  
    1.12  instance ..
    1.13  
    1.14 @@ -97,7 +97,7 @@
    1.15    \<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
    1.16    "random_fun_lift f = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of f Random.split_seed"
    1.17  
    1.18 -instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
    1.19 +instantiation "fun" :: ("{eq, term_of}", random) random
    1.20  begin
    1.21  
    1.22  definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where