src/HOL/Quickcheck_Examples/Quickcheck_Nesting_Example.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 63731 9f906a2eb0e7
permissions -rw-r--r--
executable domain membership checks
blanchet@63731
     1
theory Quickcheck_Nesting_Example
blanchet@63731
     2
imports Quickcheck_Nesting
blanchet@63731
     3
begin
blanchet@63731
     4
blanchet@63731
     5
datatype x = X "x list"
blanchet@63731
     6
blanchet@63731
     7
lemma "X a = X b"
blanchet@63731
     8
quickcheck[exhaustive, size = 4, expect = counterexample]
blanchet@63731
     9
oops
blanchet@63731
    10
blanchet@63731
    11
end