src/HOL/Nitpick_Examples/Mini_Nits.thy
changeset 54680 93f6d33a754e
parent 54633 86e0b402994c
child 54845 10df188349b3
equal deleted inserted replaced
54679:88adcd3b34e8 54680:93f6d33a754e
    11 imports Main
    11 imports Main
    12 begin
    12 begin
    13 
    13 
    14 ML_file "minipick.ML"
    14 ML_file "minipick.ML"
    15 
    15 
    16 nitpick_params [verbose, sat_solver = Riss3g, max_threads = 1]
    16 nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1]
    17 
    17 
    18 nitpick_params [total_consts = smart]
    18 nitpick_params [total_consts = smart]
    19 
    19 
    20 ML {*
    20 ML {*
    21 val check = Minipick.minipick @{context}
    21 val check = Minipick.minipick @{context}