src/HOL/ex/Quickcheck_Examples.thy
changeset 43909 7feb72f7bc3e
parent 43890 eba9c3b1f84a
child 44189 4a80017c733f
equal deleted inserted replaced
43908:e18c57d6225d 43909:7feb72f7bc3e
   348 
   348 
   349 context Truth
   349 context Truth
   350 begin
   350 begin
   351 
   351 
   352 lemma "False"
   352 lemma "False"
   353 quickcheck[expect = no_counterexample]
   353 quickcheck[exhaustive, expect = no_counterexample]
   354 oops
   354 oops
   355 
   355 
   356 end
   356 end
   357 
   357 
   358 interpretation Truth .
   358 interpretation Truth .