src/HOL/Nitpick_Examples/Core_Nits.thy
changeset 34083 652719832159
parent 34082 61b7aa37f4b7
child 34126 8a2c5d7aff51
equal deleted inserted replaced
34082:61b7aa37f4b7 34083:652719832159
     9 
     9 
    10 theory Core_Nits
    10 theory Core_Nits
    11 imports Main
    11 imports Main
    12 begin
    12 begin
    13 
    13 
    14 nitpick_params [sat_solver = MiniSatJNI]
    14 nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
    15 
    15 
    16 subsection {* Curry in a Hurry *}
    16 subsection {* Curry in a Hurry *}
    17 
    17 
    18 lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
    18 lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
    19 nitpick [card = 1\<midarrow>4, expect = none]
    19 nitpick [card = 1\<midarrow>4, expect = none]