src/HOL/Quotient.thy
changeset 36276 92011cc923f5
parent 36215 88ff48884d26
child 37049 ca1c293e521e
     1.1 --- a/src/HOL/Quotient.thy	Thu Apr 22 09:30:39 2010 +0200
     1.2 +++ b/src/HOL/Quotient.thy	Thu Apr 22 11:55:19 2010 +0200
     1.3 @@ -106,6 +106,10 @@
     1.4  where
     1.5  [simp]: "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
     1.6  
     1.7 +lemma fun_relI [intro]:
     1.8 +  assumes "\<And>a b. P a b \<Longrightarrow> Q (x a) (y b)"
     1.9 +  shows "(P ===> Q) x y"
    1.10 +  using assms by (simp add: fun_rel_def)
    1.11  
    1.12  lemma fun_map_id:
    1.13    shows "(id ---> id) = id"