equal
deleted
inserted
replaced
14 |
14 |
15 setup {* Code_Target.extend_target ("Quickcheck", (Code_Runtime.target, K I)) *} |
15 setup {* Code_Target.extend_target ("Quickcheck", (Code_Runtime.target, K I)) *} |
16 |
16 |
17 subsection {* Catching Match exceptions *} |
17 subsection {* Catching Match exceptions *} |
18 |
18 |
19 definition catch_match :: "(bool * term list) option => (bool * term list) option => (bool * term list) option" |
19 definition catch_match :: "'a => 'a => 'a" (* "(bool * term list) option => (bool * term list) option => (bool * term list) option"*) |
20 where |
20 where |
21 [code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)" |
21 [code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)" |
22 |
22 |
23 code_const catch_match |
23 code_const catch_match |
24 (Quickcheck "(_) handle Match => _") |
24 (Quickcheck "(_) handle Match => _") |