changeset 45721 | d1fb55c2ed65 |
parent 45718 | 8979b2463fc8 |
child 45729 | a709e1a0f3dd |
--- a/src/HOL/Quickcheck.thy Thu Dec 01 22:14:35 2011 +0100 +++ b/src/HOL/Quickcheck.thy Thu Dec 01 22:14:35 2011 +0100 @@ -16,7 +16,7 @@ subsection {* Catching Match exceptions *} -definition catch_match :: "term list option => term list option => term list option" +definition catch_match :: "(bool * term list) option => (bool * term list) option => (bool * term list) option" where [code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)"