src/HOL/Nitpick_Examples/Integer_Nits.thy
changeset 40341 03156257040f
parent 39362 ee65900bfced
child 41278 8e1cde88aae6
equal deleted inserted replaced
40340:d1c14898fd04 40341:03156257040f
    10 theory Integer_Nits
    10 theory Integer_Nits
    11 imports Nitpick
    11 imports Nitpick
    12 begin
    12 begin
    13 
    13 
    14 nitpick_params [card = 1\<midarrow>5, bits = 1,2,3,4,6,
    14 nitpick_params [card = 1\<midarrow>5, bits = 1,2,3,4,6,
    15                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
    15                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
    16 
    16 
    17 lemma "Suc x = x + 1"
    17 lemma "Suc x = x + 1"
    18 nitpick [unary_ints, expect = none]
    18 nitpick [unary_ints, expect = none]
    19 nitpick [binary_ints, expect = none]
    19 nitpick [binary_ints, expect = none]
    20 sorry
    20 sorry