equal
deleted
inserted
replaced
942 |
942 |
943 (* special case: global sublocale command *) |
943 (* special case: global sublocale command *) |
944 |
944 |
945 fun gen_sublocale_global prep_loc prep_interpretation |
945 fun gen_sublocale_global prep_loc prep_interpretation |
946 before_exit raw_locale expression raw_eqns thy = |
946 before_exit raw_locale expression raw_eqns thy = |
947 thy |
947 let |
948 |> Named_Target.init before_exit (prep_loc thy raw_locale) |
948 val lthy = Named_Target.init before_exit (prep_loc thy raw_locale) thy; |
949 |> gen_local_theory_interpretation prep_interpretation subscribe_locale_only expression raw_eqns; |
949 fun setup_proof after_qed = |
|
950 Element.witness_proof_eqs |
|
951 (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit); |
|
952 in |
|
953 lthy |> |
|
954 generic_interpretation prep_interpretation setup_proof |
|
955 Local_Theory.notes_kind (subscribe_locale_only lthy) expression raw_eqns |
|
956 end; |
950 |
957 |
951 in |
958 in |
952 |
959 |
953 |
960 |
954 (* interfaces *) |
961 (* interfaces *) |