src/HOL/Nitpick_Examples/Record_Nits.thy
changeset 54633 86e0b402994c
parent 48812 9509fc5485b2
child 54680 93f6d33a754e
equal deleted inserted replaced
54632:7a14f831d02d 54633:86e0b402994c
    10 theory Record_Nits
    10 theory Record_Nits
    11 imports Main
    11 imports Main
    12 begin
    12 begin
    13 
    13 
    14 nitpick_params [verbose, card = 1\<emdash>6, max_potential = 0,
    14 nitpick_params [verbose, card = 1\<emdash>6, max_potential = 0,
    15                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
    15                 sat_solver = Riss3g, max_threads = 1, timeout = 240]
    16 
    16 
    17 record point2d =
    17 record point2d =
    18   xc :: int
    18   xc :: int
    19   yc :: int
    19   yc :: int
    20 
    20