src/HOL/Library/Quotient_Syntax.thy
changeset 40602 91e583511113
parent 35787 afdf1c4958b2
child 55945 e96383acecf9
     1.1 --- a/src/HOL/Library/Quotient_Syntax.thy	Thu Nov 18 12:37:30 2010 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Syntax.thy	Thu Nov 18 17:01:15 2010 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  notation
     1.6    rel_conj (infixr "OOO" 75) and
     1.7 -  fun_map (infixr "--->" 55) and
     1.8 +  map_fun (infixr "--->" 55) and
     1.9    fun_rel (infixr "===>" 55)
    1.10  
    1.11  end