src/HOL/Predicate_Compile_Examples/List_Examples.thy
changeset 39189 d183bf90dabd
parent 39184 71f3f194b962
child 39463 7ce0ed8dc4d6
equal deleted inserted replaced
39188:cd6558ed65d7 39189:d183bf90dabd
    11    replacing =
    11    replacing =
    12      [(("appendP", "limited_appendP"), "quickcheck"),
    12      [(("appendP", "limited_appendP"), "quickcheck"),
    13       (("revP", "limited_revP"), "quickcheck"),
    13       (("revP", "limited_revP"), "quickcheck"),
    14       (("appendP", "limited_appendP"), "lim_revP")],
    14       (("appendP", "limited_appendP"), "lim_revP")],
    15    manual_reorder = [],
    15    manual_reorder = [],
       
    16    timeout = Time.fromSeconds 10,
    16    prolog_system = Code_Prolog.SWI_PROLOG}) *}
    17    prolog_system = Code_Prolog.SWI_PROLOG}) *}
    17 
    18 
    18 lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
    19 lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
    19 quickcheck[generator = code, iterations = 200000, expect = counterexample]
    20 quickcheck[generator = code, iterations = 200000, expect = counterexample]
    20 quickcheck[generator = predicate_compile_wo_ff, iterations = 1, expect = counterexample]
    21 quickcheck[generator = predicate_compile_wo_ff, iterations = 1, expect = counterexample]