src/HOL/Transfer.thy
changeset 47937 70375fa2679d
parent 47924 4e951258204b
child 48891 c0eafbd55de3
     1.1 --- a/src/HOL/Transfer.thy	Wed May 16 19:15:45 2012 +0200
     1.2 +++ b/src/HOL/Transfer.thy	Wed May 16 19:17:20 2012 +0200
     1.3 @@ -26,6 +26,11 @@
     1.4    shows "B (f x) (g y)"
     1.5    using assms by (simp add: fun_rel_def)
     1.6  
     1.7 +lemma fun_relD2:
     1.8 +  assumes "(A ===> B) f g" and "A x x"
     1.9 +  shows "B (f x) (g x)"
    1.10 +  using assms unfolding fun_rel_def by auto
    1.11 +
    1.12  lemma fun_relE:
    1.13    assumes "(A ===> B) f g" and "A x y"
    1.14    obtains "B (f x) (g y)"