--- a/src/HOL/Transfer.thy Mon May 14 17:28:07 2012 +0200
+++ b/src/HOL/Transfer.thy Tue May 15 11:50:34 2012 +0200
@@ -279,6 +279,14 @@
"(A ===> (op = ===> A) ===> op = ===> A) nat_case nat_case"
unfolding fun_rel_def by (simp split: nat.split)
+lemma nat_rec_transfer [transfer_rule]:
+ "(A ===> (op = ===> A ===> A) ===> op = ===> A) nat_rec nat_rec"
+ unfolding fun_rel_def by (clarsimp, rename_tac n, induct_tac n, simp_all)
+
+lemma funpow_transfer [transfer_rule]:
+ "(op = ===> (A ===> A) ===> (A ===> A)) compow compow"
+ unfolding funpow_def by transfer_prover
+
text {* Fallback rule for transferring universal quantifiers over
correspondence relations that are not bi-total, and do not have
custom transfer rules (e.g. relations between function types). *}