diff -r dfda74619509 -r ddd97d9dfbfb src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/Parity.thy	Thu Oct 29 11:41:36 2009 +0100
@@ -28,6 +28,13 @@
 
 end
 
+lemma transfer_int_nat_relations:
+  "even (int x) \<longleftrightarrow> even x"
+  by (simp add: even_nat_def)
+
+declare TransferMorphism_int_nat[transfer add return:
+  transfer_int_nat_relations
+]
 
 lemma even_zero_int[simp]: "even (0::int)" by presburger
 
@@ -310,6 +317,8 @@
 
 subsection {* General Lemmas About Division *}
 
+(*FIXME move to Divides.thy*)
+
 lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1" 
 apply (induct "m")
 apply (simp_all add: mod_Suc)