equal
deleted
inserted
replaced
13 |
13 |
14 subsection {* Catching Match exceptions *} |
14 subsection {* Catching Match exceptions *} |
15 |
15 |
16 axiomatization catch_match :: "'a => 'a => 'a" |
16 axiomatization catch_match :: "'a => 'a => 'a" |
17 |
17 |
18 code_const catch_match |
18 code_printing |
19 (Quickcheck "((_) handle Match => _)") |
19 constant catch_match \<rightharpoonup> (Quickcheck) "((_) handle Match => _)" |
20 |
20 |
21 subsection {* The @{text random} class *} |
21 subsection {* The @{text random} class *} |
22 |
22 |
23 class random = typerep + |
23 class random = typerep + |
24 fixes random :: "natural \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed" |
24 fixes random :: "natural \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed" |
210 setup Random_Generators.setup |
210 setup Random_Generators.setup |
211 |
211 |
212 |
212 |
213 subsection {* Code setup *} |
213 subsection {* Code setup *} |
214 |
214 |
215 code_const random_fun_aux (Quickcheck "Random'_Generators.random'_fun") |
215 code_printing |
|
216 constant random_fun_aux \<rightharpoonup> (Quickcheck) "Random'_Generators.random'_fun" |
216 -- {* With enough criminal energy this can be abused to derive @{prop False}; |
217 -- {* With enough criminal energy this can be abused to derive @{prop False}; |
217 for this reason we use a distinguished target @{text Quickcheck} |
218 for this reason we use a distinguished target @{text Quickcheck} |
218 not spoiling the regular trusted code generation *} |
219 not spoiling the regular trusted code generation *} |
219 |
220 |
220 code_reserved Quickcheck Random_Generators |
221 code_reserved Quickcheck Random_Generators |