--- 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)