Attic/Quot/Quotient_Syntax.thy
branchNominal2-Isabelle2013
changeset 3208 da575186d492
parent 3206 fb201e383f1b
child 3209 2fb0bc0dcbf1
equal deleted inserted replaced
3206:fb201e383f1b 3208:da575186d492
     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 (*>*)