src/HOL/Quickcheck.thy
changeset 48273 65233084e9d7
parent 46976 80123a220219
child 48891 c0eafbd55de3
equal deleted inserted replaced
48272:db75b4005d9a 48273:65233084e9d7
    17 subsection {* Catching Match exceptions *}
    17 subsection {* Catching Match exceptions *}
    18 
    18 
    19 axiomatization catch_match :: "'a => 'a => 'a"
    19 axiomatization catch_match :: "'a => 'a => 'a"
    20 
    20 
    21 code_const catch_match 
    21 code_const catch_match 
    22   (Quickcheck "(_) handle Match => _")
    22   (Quickcheck "((_) handle Match => _)")
    23 
    23 
    24 subsection {* The @{text random} class *}
    24 subsection {* The @{text random} class *}
    25 
    25 
    26 class random = typerep +
    26 class random = typerep +
    27   fixes random :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
    27   fixes random :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"