wneuper/isa: src/HOL/Library/Quotient

src/HOL/Library/Quotient_Syntax.thy

library theories for debugging and parallel computing using code generation towards Isabelle/ML

     1 (*  Title:      HOL/Library/Quotient_Syntax.thy

     2     Author:     Cezary Kaliszyk and Christian Urban

     3 *)

     5 header {* Pretty syntax for Quotient operations *}

     7 theory Quotient_Syntax

     8 imports Main

     9 begin

    11 notation

    12   rel_conj (infixr "OOO" 75) and

    13   map_fun (infixr "--->" 55) and

    14   fun_rel (infixr "===>" 55)

    16 end

wneuper/isa