src/HOL/Parity.thy
changeset 35644 d20cf282342e
parent 35631 0b8a5fd339ab
child 36722 c8ea75ea4a29
equal deleted inserted replaced
35643:965c24dd6856 35644:d20cf282342e
    30 
    30 
    31 lemma transfer_int_nat_relations:
    31 lemma transfer_int_nat_relations:
    32   "even (int x) \<longleftrightarrow> even x"
    32   "even (int x) \<longleftrightarrow> even x"
    33   by (simp add: even_nat_def)
    33   by (simp add: even_nat_def)
    34 
    34 
    35 declare TransferMorphism_int_nat[transfer add return:
    35 declare transfer_morphism_int_nat[transfer add return:
    36   transfer_int_nat_relations
    36   transfer_int_nat_relations
    37 ]
    37 ]
    38 
    38 
    39 lemma even_zero_int[simp]: "even (0::int)" by presburger
    39 lemma even_zero_int[simp]: "even (0::int)" by presburger
    40 
    40