--- a/src/HOL/Transfer.thy Tue Apr 17 09:12:15 2012 +0200
+++ b/src/HOL/Transfer.thy Tue Apr 17 11:03:08 2012 +0200
@@ -88,6 +88,8 @@
setup Transfer.setup
+declare fun_rel_eq [relator_eq]
+
lemma Rel_App [transfer_raw]:
assumes "Rel (A ===> B) f g" and "Rel A x y"
shows "Rel B (App f x) (App g y)"