1.1 --- a/src/HOL/Quotient.thy	Fri Nov 19 10:37:06 2010 +0100
     1.2 +++ b/src/HOL/Quotient.thy	Fri Nov 19 11:44:46 2010 +0100
     1.3 @@ -167,7 +167,7 @@
     1.4    by (simp add: fun_eq_iff)
     1.5  
     1.6  definition
     1.7 -  fun_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" (infixr "===>" 55)
     1.8 +  fun_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool" (infixr "===>" 55)
     1.9  where
    1.10    "fun_rel E1 E2 = (\<lambda>f g. \<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
    1.11