src/HOL/Library/Quotient_Syntax.thy
changeset 55945 e96383acecf9
parent 40602 91e583511113
child 58881 b9556a055632
--- a/src/HOL/Library/Quotient_Syntax.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Library/Quotient_Syntax.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -11,6 +11,6 @@
 notation
   rel_conj (infixr "OOO" 75) and
   map_fun (infixr "--->" 55) and
-  fun_rel (infixr "===>" 55)
+  rel_fun (infixr "===>" 55)
 
 end