Attic/Quot/Quotient_Syntax.thy
branchNominal2-Isabelle2011-1
changeset 3069 78d828f43cdf
parent 3068 f89ee40fbb08
child 3070 4b4742aa43f2
equal deleted inserted replaced
3068:f89ee40fbb08 3069:78d828f43cdf
     1 (*  Title:      Quotient_Syntax.thy
       
     2     Author:     Cezary Kaliszyk and Christian Urban
       
     3 *)
       
     4 
       
     5 header {* Pretty syntax for Quotient operations *}
       
     6 
       
     7 (*<*)
       
     8 theory Quotient_Syntax
       
     9 imports Quotient
       
    10 begin
       
    11 
       
    12 notation
       
    13   rel_conj (infixr "OOO" 75) and
       
    14   fun_map (infixr "--->" 55) and
       
    15   fun_rel (infixr "===>" 55)
       
    16 
       
    17 end
       
    18 (*>*)