equal
deleted
inserted
replaced
143 |
143 |
144 val get_silent = #silent o NameSpaceData.get; |
144 val get_silent = #silent o NameSpaceData.get; |
145 |
145 |
146 fun prove_interpretation_in ctxt_tac (name, expr) thy = |
146 fun prove_interpretation_in ctxt_tac (name, expr) thy = |
147 thy |
147 thy |
148 |> Expression.sublocale_cmd name expr |
148 |> Expression.sublocale_cmd name expr [] |
149 |> Proof.global_terminal_proof |
149 |> Proof.global_terminal_proof |
150 (Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), NONE) |
150 (Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), NONE) |
151 |> ProofContext.theory_of |
151 |> ProofContext.theory_of |
152 |
152 |
153 fun add_locale name expr elems thy = |
153 fun add_locale name expr elems thy = |