190 (interpretation * model * arguments) option)) list, |
190 (interpretation * model * arguments) option)) list, |
191 printers: (string * (Proof.context -> model -> typ -> interpretation -> |
191 printers: (string * (Proof.context -> model -> typ -> interpretation -> |
192 (int -> bool) -> term option)) list, |
192 (int -> bool) -> term option)) list, |
193 parameters: string Symtab.table}; |
193 parameters: string Symtab.table}; |
194 val empty = {interpreters = [], printers = [], parameters = Symtab.empty}; |
194 val empty = {interpreters = [], printers = [], parameters = Symtab.empty}; |
195 val extend = I; |
|
196 fun merge |
195 fun merge |
197 ({interpreters = in1, printers = pr1, parameters = pa1}, |
196 ({interpreters = in1, printers = pr1, parameters = pa1}, |
198 {interpreters = in2, printers = pr2, parameters = pa2}) : T = |
197 {interpreters = in2, printers = pr2, parameters = pa2}) : T = |
199 {interpreters = AList.merge (op =) (K true) (in1, in2), |
198 {interpreters = AList.merge (op =) (K true) (in1, in2), |
200 printers = AList.merge (op =) (K true) (pr1, pr2), |
199 printers = AList.merge (op =) (K true) (pr1, pr2), |