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