src/HOL/Nitpick_Examples/Manual_Nits.thy
changeset 35075 6fd1052fe463
parent 35073 cc19e2aef17e
child 35180 c57dba973391
equal deleted inserted replaced
35074:c1dac8ace020 35075:6fd1052fe463
    11 imports Main Coinductive_List RealDef
    11 imports Main Coinductive_List RealDef
    12 begin
    12 begin
    13 
    13 
    14 chapter {* 3. First Steps *}
    14 chapter {* 3. First Steps *}
    15 
    15 
    16 nitpick_params [sat_solver = MiniSatJNI, max_threads = 1]
    16 nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1]
    17 
    17 
    18 subsection {* 3.1. Propositional Logic *}
    18 subsection {* 3.1. Propositional Logic *}
    19 
    19 
    20 lemma "P \<longleftrightarrow> Q"
    20 lemma "P \<longleftrightarrow> Q"
    21 nitpick
    21 nitpick