src/HOL/Quickcheck_Exhaustive.thy
changeset 52435 6646bb548c6b
parent 51143 0a2371e7ced3
child 53015 a1119cf551e8
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Sun Jun 23 21:16:06 2013 +0200
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Sun Jun 23 21:16:07 2013 +0200
     1.3 @@ -518,10 +518,11 @@
     1.4  axiomatization throw_Counterexample :: "term list => unit"
     1.5  axiomatization catch_Counterexample :: "unit => term list option"
     1.6  
     1.7 -code_const throw_Counterexample
     1.8 -  (Quickcheck "raise (Exhaustive'_Generators.Counterexample _)")
     1.9 -code_const catch_Counterexample
    1.10 -  (Quickcheck "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts => SOME ts)")
    1.11 +code_printing
    1.12 +  constant throw_Counterexample \<rightharpoonup>
    1.13 +    (Quickcheck) "raise (Exhaustive'_Generators.Counterexample _)"
    1.14 +| constant catch_Counterexample \<rightharpoonup>
    1.15 +    (Quickcheck) "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts => SOME ts)"
    1.16  
    1.17  subsection {* Continuation passing style functions as plus monad *}
    1.18