src/HOL/Predicate_Compile_Examples/List_Examples.thy
changeset 40924 a9be7f26b4e6
parent 40137 9eabcb1bfe50
child 41413 64cd30d6b0b8
equal deleted inserted replaced
40923:be80c93ac0a2 40924:a9be7f26b4e6
    14       (("revP", "limited_revP"), "quickcheck"),
    14       (("revP", "limited_revP"), "quickcheck"),
    15       (("appendP", "limited_appendP"), "lim_revP")],
    15       (("appendP", "limited_appendP"), "lim_revP")],
    16    manual_reorder = []}) *}
    16    manual_reorder = []}) *}
    17 
    17 
    18 lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
    18 lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
    19 quickcheck[generator = code, iterations = 10000]
    19 quickcheck[tester = random, iterations = 10000]
    20 quickcheck[generator = predicate_compile_wo_ff, iterations = 1, expect = counterexample]
    20 quickcheck[tester = predicate_compile_wo_ff, iterations = 1, expect = counterexample]
    21 quickcheck[generator = prolog, expect = counterexample]
    21 quickcheck[tester = prolog, expect = counterexample]
    22 oops
    22 oops
    23 
    23 
    24 end
    24 end