equal
deleted
inserted
replaced
147 |
147 |
148 fun prove_interpretation_in ctxt_tac (name, expr) thy = |
148 fun prove_interpretation_in ctxt_tac (name, expr) thy = |
149 thy |
149 thy |
150 |> Expression.sublocale_cmd name expr |
150 |> Expression.sublocale_cmd name expr |
151 |> Proof.global_terminal_proof |
151 |> Proof.global_terminal_proof |
152 (Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt),Position.none), NONE) |
152 (Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), NONE) |
153 |> ProofContext.theory_of |
153 |> ProofContext.theory_of |
154 |
154 |
155 fun add_locale name expr elems thy = |
155 fun add_locale name expr elems thy = |
156 thy |
156 thy |
157 |> Expression.add_locale (Binding.name name) (Binding.name name) expr elems |
157 |> Expression.add_locale (Binding.name name) (Binding.name name) expr elems |