equal
deleted
inserted
replaced
21 replacing = [], |
21 replacing = [], |
22 manual_reorder = []}) *} |
22 manual_reorder = []}) *} |
23 |
23 |
24 values 40 "{s. hotel s}" |
24 values 40 "{s. hotel s}" |
25 |
25 |
26 setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *} |
26 setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *} |
27 |
27 |
28 lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g" |
28 lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g" |
29 quickcheck[tester = random, iterations = 10000, report] |
29 quickcheck[tester = random, iterations = 10000, report] |
30 quickcheck[tester = prolog, iterations = 1, expect = counterexample] |
30 quickcheck[tester = prolog, iterations = 1, expect = counterexample] |
31 oops |
31 oops |