1 

     1 

     2 signature QUOTIENT_DEF =

     2 signature QUOTIENT_DEF =

     3 sig 

     3 sig 

     4   val quotient_def: mixfix -> Attrib.binding -> term -> term ->

     4   val quotient_def: mixfix -> Attrib.binding -> term -> term ->

     5     local_theory -> (term * thm) * local_theory

     5     local_theory -> (term * thm) * local_theory

     6   val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) ->

     7   val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) ->

     7     local_theory -> local_theory

     8     local_theory -> local_theory

     8 end;

     9 end;

     9 

    10 

    10 structure Quotient_Def: QUOTIENT_DEF =

    11 structure Quotient_Def: QUOTIENT_DEF =