src/HOL/Nitpick_Examples/Pattern_Nits.thy
changeset 40341 03156257040f
parent 35284 9edc2bd6d2bd
child 41278 8e1cde88aae6
equal deleted inserted replaced
40340:d1c14898fd04 40341:03156257040f
    10 theory Pattern_Nits
    10 theory Pattern_Nits
    11 imports Main
    11 imports Main
    12 begin
    12 begin
    13 
    13 
    14 nitpick_params [card = 10, max_potential = 0, sat_solver = MiniSat_JNI,
    14 nitpick_params [card = 10, max_potential = 0, sat_solver = MiniSat_JNI,
    15                 max_threads = 1, timeout = 60 s]
    15                 max_threads = 1, timeout = 60]
    16 
    16 
    17 lemma "x = (case u of () \<Rightarrow> y)"
    17 lemma "x = (case u of () \<Rightarrow> y)"
    18 nitpick [expect = genuine]
    18 nitpick [expect = genuine]
    19 oops
    19 oops
    20 
    20