src/HOL/Nitpick_Examples/Integer_Nits.thy
changeset 46090 f1796596ef60
parent 45035 60d2c03d5c70
child 47108 2a1953f0d20d
equal deleted inserted replaced
46089:d98eb715444d 46090:f1796596ef60
     3     Copyright   2009-2011
     3     Copyright   2009-2011
     4 
     4 
     5 Examples featuring Nitpick applied to natural numbers and integers.
     5 Examples featuring Nitpick applied to natural numbers and integers.
     6 *)
     6 *)
     7 
     7 
     8 header {* Examples Featuring Nitpick Applied to Natural Numbers and Integers *} 
     8 header {* Examples Featuring Nitpick Applied to Natural Numbers and Integers *}
     9 
     9 
    10 theory Integer_Nits
    10 theory Integer_Nits
    11 imports Nitpick
    11 imports Main
    12 begin
    12 begin
    13 
    13 
    14 nitpick_params [verbose, card = 1\<emdash>5, bits = 1,2,3,4,6,
    14 nitpick_params [verbose, card = 1\<emdash>5, bits = 1,2,3,4,6,
    15                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
    15                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
    16 
    16