equal
deleted
inserted
replaced
19 type qconsts_info = {qconst: term, rconst: term, def: thm} |
19 type qconsts_info = {qconst: term, rconst: term, def: thm} |
20 val transform_qconsts: morphism -> qconsts_info -> qconsts_info |
20 val transform_qconsts: morphism -> qconsts_info -> qconsts_info |
21 val qconsts_lookup: theory -> term -> qconsts_info (* raises NotFound *) |
21 val qconsts_lookup: theory -> term -> qconsts_info (* raises NotFound *) |
22 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
22 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
23 val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic |
23 val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic |
24 val qconsts_dest: theory -> qconsts_info list |
24 val qconsts_dest: Proof.context -> qconsts_info list |
25 val print_qconstinfo: Proof.context -> unit |
25 val print_qconstinfo: Proof.context -> unit |
26 |
26 |
27 val equiv_rules_get: Proof.context -> thm list |
27 val equiv_rules_get: Proof.context -> thm list |
28 val equiv_rules_add: attribute |
28 val equiv_rules_add: attribute |
29 val rsp_rules_get: Proof.context -> thm list |
29 val rsp_rules_get: Proof.context -> thm list |
196 def = Morphism.thm phi def} |
196 def = Morphism.thm phi def} |
197 |
197 |
198 fun qconsts_update_thy name qcinfo = QConstsData.map (Symtab.cons_list (name, qcinfo)) |
198 fun qconsts_update_thy name qcinfo = QConstsData.map (Symtab.cons_list (name, qcinfo)) |
199 fun qconsts_update_gen name qcinfo = Context.mapping (qconsts_update_thy name qcinfo) I |
199 fun qconsts_update_gen name qcinfo = Context.mapping (qconsts_update_thy name qcinfo) I |
200 |
200 |
201 fun qconsts_dest thy = |
201 fun qconsts_dest lthy = |
202 flat (map snd (Symtab.dest (QConstsData.get thy))) |
202 flat (map snd (Symtab.dest (QConstsData.get (ProofContext.theory_of lthy)))) |
203 |
203 |
204 fun qconsts_lookup thy t = |
204 fun qconsts_lookup thy t = |
205 let |
205 let |
206 val (name, qty) = dest_Const t |
206 val (name, qty) = dest_Const t |
207 fun matches x = |
207 fun matches x = |