10   val quotdata_lookup_thy: theory -> string -> quotient_info option

    10   val quotdata_lookup_thy: theory -> string -> quotient_info option

    11   val quotdata_lookup: Proof.context -> string -> quotient_info option

    11   val quotdata_lookup: Proof.context -> string -> quotient_info option

    12   val quotdata_update_thy: string -> (typ * typ * term * thm) -> theory -> theory

    12   val quotdata_update_thy: string -> (typ * typ * term * thm) -> theory -> theory

    13   val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context

    13   val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context

    14 

    14 

    15   type qenv = (typ * typ) list

    16   type qenv = (typ * typ) list

    16   val mk_qenv: Proof.context -> qenv

    17   val mk_qenv: Proof.context -> qenv

    17   val lookup_qenv: ((typ * typ) -> bool) -> qenv -> typ -> (typ * typ) option

    18   val lookup_qenv: ((typ * typ) -> bool) -> qenv -> typ -> (typ * typ) option

    18 

    19 

    19   type qconsts_info = {qconst: term, rconst: term}

    20   type qconsts_info = {qconst: term, rconst: term}