equal
deleted
inserted
replaced
231 (case Element.eq_morphism thy thms of |
231 (case Element.eq_morphism thy thms of |
232 SOME eq_morph => |
232 SOME eq_morph => |
233 fold (fn cls => fn thy => |
233 fold (fn cls => fn thy => |
234 Context.theory_map |
234 Context.theory_map |
235 (Locale.amend_registration |
235 (Locale.amend_registration |
236 {dep = (cls, base_morphism thy cls), |
236 {inst = (cls, base_morphism thy cls), |
237 mixin = SOME (eq_morph, true), |
237 mixin = SOME (eq_morph, true), |
238 export = export_morphism thy cls}) thy) (heritage thy [class]) thy |
238 export = export_morphism thy cls}) thy) (heritage thy [class]) thy |
239 | NONE => thy); |
239 | NONE => thy); |
240 |
240 |
241 fun register_operation class (c, t) input_only thy = |
241 fun register_operation class (c, t) input_only thy = |
490 |> filter (is_class thy); |
490 |> filter (is_class thy); |
491 val add_dependency = |
491 val add_dependency = |
492 (case some_dep_morph of |
492 (case some_dep_morph of |
493 SOME dep_morph => |
493 SOME dep_morph => |
494 Generic_Target.locale_dependency sub |
494 Generic_Target.locale_dependency sub |
495 {dep = (sup, dep_morph $> Element.satisfy_morphism (the_list some_witn)), |
495 {inst = (sup, dep_morph $> Element.satisfy_morphism (the_list some_witn)), |
496 mixin = NONE, export = export} |
496 mixin = NONE, export = export} |
497 | NONE => I); |
497 | NONE => I); |
498 in |
498 in |
499 lthy |
499 lthy |
500 |> Local_Theory.raw_theory |
500 |> Local_Theory.raw_theory |