equal
deleted
inserted
replaced
11 type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} |
11 type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} |
12 val quotdata_transfer: morphism -> quotdata_info -> quotdata_info |
12 val quotdata_transfer: morphism -> quotdata_info -> quotdata_info |
13 val quotdata_lookup: theory -> string -> quotdata_info (* raises NotFound *) |
13 val quotdata_lookup: theory -> string -> quotdata_info (* raises NotFound *) |
14 val quotdata_update_thy: string -> quotdata_info -> theory -> theory |
14 val quotdata_update_thy: string -> quotdata_info -> theory -> theory |
15 val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic |
15 val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic |
16 val quotdata_dest: theory -> quotdata_info list |
|
17 val print_quotinfo: Proof.context -> unit |
16 val print_quotinfo: Proof.context -> unit |
18 |
17 |
19 type qconsts_info = {qconst: term, rconst: term, def: thm} |
18 type qconsts_info = {qconst: term, rconst: term, def: thm} |
20 val qconsts_transfer: morphism -> qconsts_info -> qconsts_info |
19 val qconsts_transfer: morphism -> qconsts_info -> qconsts_info |
21 val qconsts_lookup: theory -> term -> qconsts_info (* raises NotFound *) |
20 val qconsts_lookup: theory -> term -> qconsts_info (* raises NotFound *) |