src/HOL/Nitpick_Examples/Core_Nits.thy
changeset 41278 8e1cde88aae6
parent 40341 03156257040f
child 42208 02513eb26eb7
equal deleted inserted replaced
41277:1369c27c6966 41278:8e1cde88aae6
     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 [card = 1\<midarrow>6, unary_ints, max_potential = 0,
    14 nitpick_params [verbose, card = 1\<midarrow>6, unary_ints, max_potential = 0,
    15                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
    15                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
    16 
    16 
    17 subsection {* Curry in a Hurry *}
    17 subsection {* Curry in a Hurry *}
    18 
    18 
    19 lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
    19 lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"