src/HOL/Quickcheck_Exhaustive.thy
changeset 45684 3d6ee9c7d7ef
parent 45450 dc2236b19a3d
child 45697 3b7c35a08723
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Wed Nov 30 09:21:07 2011 +0100
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Wed Nov 30 09:21:09 2011 +0100
     1.3 @@ -530,6 +530,15 @@
     1.4  code_const catch_match 
     1.5    (Quickcheck "(_) handle Match => _")
     1.6  
     1.7 +definition catch_match' :: "term => term => term"
     1.8 +where
     1.9 +  [code del]: "catch_match' t1 t2 = (SOME t. t = t1 \<or> t = t2)"
    1.10 +
    1.11 +code_const catch_match'
    1.12 +  (Quickcheck "(_) handle Match => _")
    1.13 +
    1.14 +consts unknown :: "'a" ("?")
    1.15 + 
    1.16  use "Tools/Quickcheck/exhaustive_generators.ML"
    1.17  
    1.18  setup {* Exhaustive_Generators.setup *}