diff -r 04d9381bebff -r a4d81cdebf8b src/HOL/ex/Transfer_Int_Nat.thy
--- a/src/HOL/ex/Transfer_Int_Nat.thy	Mon May 13 12:13:24 2013 +0200
+++ b/src/HOL/ex/Transfer_Int_Nat.thy	Mon May 13 13:59:04 2013 +0200
@@ -13,6 +13,11 @@
 definition ZN :: "int \<Rightarrow> nat \<Rightarrow> bool"
   where "ZN = (\<lambda>z n. z = of_nat n)"
 
+subsection {* Transfer domain rules *}
+
+lemma Domainp_ZN [transfer_domain_rule]: "Domainp ZN = (\<lambda>x. x \<ge> 0)" 
+  unfolding ZN_def Domainp_iff[abs_def] by (auto intro: zero_le_imp_eq_int)
+
 subsection {* Transfer rules *}
 
 lemma bi_unique_ZN [transfer_rule]: "bi_unique ZN"
@@ -155,11 +160,11 @@
 apply fact
 done
 
-text {* Quantifiers over higher types (e.g. @{text "nat list"}) may
-  generate @{text "Domainp"} assumptions when transferred. *}
+text {* Quantifiers over higher types (e.g. @{text "nat list"}) are
+  transferred to a readable formula thanks to the transfer domain rule @{thm Domainp_ZN} *}
 
 lemma
-  assumes "\<And>xs::int list. Domainp (list_all2 ZN) xs \<Longrightarrow>
+  assumes "\<And>xs::int list. list_all (\<lambda>x. x \<ge> 0) xs \<Longrightarrow>
     (listsum xs = 0) = list_all (\<lambda>x. x = 0) xs"
   shows "listsum xs = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) xs"
 apply transfer
@@ -170,7 +175,7 @@
   involved are bi-unique. *}
 
 lemma
-  assumes "\<And>xs\<Colon>int list. \<lbrakk>Domainp (list_all2 ZN) xs; xs \<noteq> []\<rbrakk> \<Longrightarrow>
+  assumes "\<And>xs\<Colon>int list. \<lbrakk>list_all (\<lambda>x. x \<ge> 0) xs; xs \<noteq> []\<rbrakk> \<Longrightarrow>
     listsum xs < listsum (map (\<lambda>x. x + 1) xs)"
   shows "xs \<noteq> [] \<Longrightarrow> listsum xs < listsum (map Suc xs)"
 apply transfer