equal
deleted
inserted
replaced
15 |
15 |
16 type qconsts_info = {qconst: term, rconst: term, def: thm} |
16 type qconsts_info = {qconst: term, rconst: term, def: thm} |
17 val qconsts_transfer: morphism -> qconsts_info -> qconsts_info |
17 val qconsts_transfer: morphism -> qconsts_info -> qconsts_info |
18 val qconsts_lookup: theory -> string -> qconsts_info option |
18 val qconsts_lookup: theory -> string -> qconsts_info option |
19 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
19 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
20 val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic |
20 val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic |
|
21 val qconsts_dest: theory -> qconsts_info list |
21 val print_qconstinfo: Proof.context -> unit |
22 val print_qconstinfo: Proof.context -> unit |
22 |
23 |
23 val rsp_rules_get: Proof.context -> thm list |
24 val rsp_rules_get: Proof.context -> thm list |
24 end; |
25 end; |
25 |
26 |
134 val qconsts_lookup = Symtab.lookup o QConstsData.get |
135 val qconsts_lookup = Symtab.lookup o QConstsData.get |
135 |
136 |
136 fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo)) |
137 fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo)) |
137 fun qconsts_update_gen k qcinfo = Context.mapping (qconsts_update_thy k qcinfo) I |
138 fun qconsts_update_gen k qcinfo = Context.mapping (qconsts_update_thy k qcinfo) I |
138 |
139 |
|
140 fun qconsts_dest thy = |
|
141 map snd (Symtab.dest (QConstsData.get thy)) |
|
142 |
139 (* We don't print the definition *) |
143 (* We don't print the definition *) |
140 fun print_qconstinfo ctxt = |
144 fun print_qconstinfo ctxt = |
141 let |
145 let |
142 fun prt_qconst {qconst, rconst, def} = |
146 fun prt_qconst {qconst, rconst, def} = |
143 Pretty.block (separate (Pretty.brk 1) |
147 Pretty.block (separate (Pretty.brk 1) |