812 |
812 |
813 (** Interpretation in theories and proof contexts **) |
813 (** Interpretation in theories and proof contexts **) |
814 |
814 |
815 local |
815 local |
816 |
816 |
817 fun note_eqns_register deps witss attrss eqns export export' context = |
817 fun note_eqns_register deps witss attrss eqns export export' = |
818 context |
818 Element.generic_note_thmss Thm.lemmaK |
819 |> Element.generic_note_thmss Thm.lemmaK |
|
820 (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns) |
819 (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns) |
821 |-> (fn facts => `(fn context => meta_rewrite (Context.proof_of context) (maps snd facts))) |
820 #-> (fn facts => `(fn context => meta_rewrite (Context.proof_of context) (maps snd facts))) |
822 |-> (fn eqns => fold (fn ((dep, morph), wits) => |
821 #-> (fn eqns => fold (fn ((dep, morph), wits) => |
823 fn context => |
822 fn context => |
824 Locale.add_registration (dep, morph $> Element.satisfy_morphism |
823 Locale.add_registration |
825 (map (Element.transform_witness export') wits)) |
824 (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)) |
826 (Element.eq_morphism (Context.theory_of context) eqns |> |
825 (Element.eq_morphism (Context.theory_of context) eqns |> Option.map (rpair true)) |
827 Option.map (rpair true)) |
|
828 export context) (deps ~~ witss)); |
826 export context) (deps ~~ witss)); |
829 |
827 |
830 fun gen_interpretation prep_expr parse_prop prep_attr |
828 fun gen_interpretation prep_expr parse_prop prep_attr |
831 expression equations thy = |
829 expression equations thy = |
832 let |
830 let |