equal
deleted
inserted
replaced
32 oops |
32 oops |
33 |
33 |
34 lemma |
34 lemma |
35 "x \<in> {1, 2} \<union> {3, 4} ==> x = (1::nat) \<or> x = (2::nat)" |
35 "x \<in> {1, 2} \<union> {3, 4} ==> x = (1::nat) \<or> x = (2::nat)" |
36 quickcheck[generator=predicate_compile_wo_ff] |
36 quickcheck[generator=predicate_compile_wo_ff] |
|
37 oops |
|
38 |
|
39 section {* Equivalences *} |
|
40 |
|
41 inductive is_ten :: "nat => bool" |
|
42 where |
|
43 "is_ten 10" |
|
44 |
|
45 inductive is_eleven :: "nat => bool" |
|
46 where |
|
47 "is_eleven 11" |
|
48 |
|
49 lemma |
|
50 "is_ten x = is_eleven x" |
|
51 quickcheck[generator = predicate_compile_wo_ff, iterations = 1, size = 1, expect = counterexample] |
37 oops |
52 oops |
38 |
53 |
39 section {* Context Free Grammar *} |
54 section {* Context Free Grammar *} |
40 |
55 |
41 datatype alphabet = a | b |
56 datatype alphabet = a | b |