src/HOL/Transfer.thy
changeset 47503 cb44d09d9d22
parent 47355 3d9d98e0f1a4
child 47523 1bf0e92c1ca0
     1.1 --- a/src/HOL/Transfer.thy	Tue Apr 17 09:12:15 2012 +0200
     1.2 +++ b/src/HOL/Transfer.thy	Tue Apr 17 11:03:08 2012 +0200
     1.3 @@ -88,6 +88,8 @@
     1.4  
     1.5  setup Transfer.setup
     1.6  
     1.7 +declare fun_rel_eq [relator_eq]
     1.8 +
     1.9  lemma Rel_App [transfer_raw]:
    1.10    assumes "Rel (A ===> B) f g" and "Rel A x y"
    1.11    shows "Rel B (App f x) (App g y)"