# HG changeset patch
# User haftmann
# Date 1290163486 -3600
# Node ID ab551d108feb96841e4f91758a3d2001c9e143b7
# Parent  d6eeffa0d9a0c4d652fd0d24880e074b6870fa4f
generalized type

diff -r d6eeffa0d9a0 -r ab551d108feb src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Fri Nov 19 10:37:06 2010 +0100
+++ b/src/HOL/Quotient.thy	Fri Nov 19 11:44:46 2010 +0100
@@ -167,7 +167,7 @@
   by (simp add: fun_eq_iff)
 
 definition
-  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)
+  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)
 where
   "fun_rel E1 E2 = (\<lambda>f g. \<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"