src/HOL/Main.thy
changeset 14192 d6cb80cc1d20
parent 14102 8af7334af4b3
child 14350 41b32020d0b3
equal deleted inserted replaced
14191:2014eac694d2 14192:d6cb80cc1d20
    86 *}
    86 *}
    87 
    87 
    88 setup eq_codegen_setup
    88 setup eq_codegen_setup
    89 
    89 
    90 lemma [code]: "((n::nat) < 0) = False" by simp
    90 lemma [code]: "((n::nat) < 0) = False" by simp
    91 lemmas [code] = less_Suc_eq imp_conv_disj
    91 lemma [code]: "(0 < Suc n) = True" by simp
       
    92 lemmas [code] = Suc_less_eq imp_conv_disj
    92 
    93 
    93 end
    94 end